diff options
Diffstat (limited to 'library')
37 files changed, 338 insertions, 70 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml new file mode 100644 index 00000000..9ce22b09 --- /dev/null +++ b/library/assumptions.ml @@ -0,0 +1,238 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* The following definitions are used by the function + [assumptions] which gives as an output the set of all + axioms and sections variables on which a given term depends + in a context (expectingly the Global context) *) + +(* Initial author: Arnaud Spiwack + Module-traversing code: Pierre Letouzey *) + +open Util +open Names +open Sign +open Univ +open Term +open Declarations +open Mod_subst + +type context_object = + | Variable of identifier (* A section variable or a Let definition *) + | Axiom of constant (* An axiom or a constant. *) + | Opaque of constant (* An opaque constant. *) + +(* Defines a set of [assumption] *) +module OrderedContextObject = +struct + type t = context_object + let compare x y = + match x , y with + | Variable i1 , Variable i2 -> id_ord i1 i2 + | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2 + (* spiwack: it would probably be cleaner + to provide a [kn_ord] function *) + | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2 + | Variable _ , Axiom _ -> -1 + | Axiom _ , Variable _ -> 1 + | Opaque _ , _ -> -1 + | _, Opaque _ -> 1 +end + +module ContextObjectSet = Set.Make (OrderedContextObject) +module ContextObjectMap = Map.Make (OrderedContextObject) + +(** For a constant c in a module sealed by an interface (M:T and + not M<:T), [Global.lookup_constant] may return a [constant_body] + without body. We fix this by looking in the implementation + of the module *) + +let modcache = ref (MPmap.empty : structure_body MPmap.t) + +let rec lookup_module_in_impl mp = + try Global.lookup_module mp + with Not_found -> + (* The module we search might not be exported by its englobing module(s). + We access the upper layer, and then do a manual search *) + match mp with + | MPfile _ | MPbound _ -> + raise Not_found (* should have been found by [lookup_module] *) + | MPdot (mp',lab') -> + let fields = memoize_fields_of_mp mp' in + match List.assoc lab' fields with + | SFBmodule mb -> mb + | _ -> assert false (* same label for a non-module ?! *) + +and memoize_fields_of_mp mp = + try MPmap.find mp !modcache + with Not_found -> + let l = fields_of_mp mp in + modcache := MPmap.add mp l !modcache; + l + +and fields_of_mp mp = + let mb = lookup_module_in_impl mp in + let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in + let subs = + if inner_mp = mp then subs + else add_mp inner_mp mp mb.mod_delta subs + in + Modops.subst_signature subs fields + +and fields_of_mb subs mb args = + let seb = match mb.mod_expr with + | None -> mb.mod_type (* cf. Declare Module *) + | Some seb -> seb + in + fields_of_seb subs mb.mod_mp seb args + +(* TODO: using [empty_delta_resolver] below in [fields_of_seb] + is probably slightly incorrect. But: + a) I don't see currently what should be used instead + b) this shouldn't be critical for Print Assumption. At worse some + constants will have a canonical name which is non-canonical, + leading to failures in [Global.lookup_constant], but our own + [lookup_constant] should work. +*) + +and fields_of_seb subs mp0 seb args = match seb with + | SEBstruct l -> + assert (args = []); + l, mp0, subs + | SEBident mp -> + let mb = lookup_module_in_impl (subst_mp subs mp) in + fields_of_mb subs mb args + | SEBapply (seb1,seb2,_) -> + (match seb2 with + | SEBident mp2 -> fields_of_seb subs mp0 seb1 (mp2::args) + | _ -> assert false) (* only legal application is to module names *) + | SEBfunctor (mbid,mtb,seb) -> + (match args with + | [] -> assert false (* we should only encounter applied functors *) + | mpa :: args -> + let subs = add_mbid mbid mpa empty_delta_resolver subs in + fields_of_seb subs mp0 seb args) + | SEBwith _ -> assert false (* should not appear in a mod_expr + or mod_type field *) + +let lookup_constant_in_impl cst fallback = + try + let mp,dp,lab = repr_kn (canonical_con cst) in + let fields = memoize_fields_of_mp mp in + (* A module found this way is necessarily closed, in particular + our constant cannot be in an opened section : *) + match List.assoc lab fields with + | SFBconst cb -> cb + | _ -> assert false (* label not pointing to a constant ?! *) + with Not_found -> + (* Either: + - The module part of the constant isn't registered yet : + we're still in it, so the [constant_body] found earlier + (if any) was a true axiom. + - The label has not been found in the structure. This is an error *) + match fallback with + | Some cb -> cb + | None -> anomaly ("Print Assumption: unknown constant "^string_of_con cst) + +let lookup_constant cst = + try + let cb = Global.lookup_constant cst in + if cb.const_body <> None then cb + else lookup_constant_in_impl cst (Some cb) + with Not_found -> lookup_constant_in_impl cst None + +let assumptions ?(add_opaque=false) st (* t *) = + modcache := MPmap.empty; + let (idts,knst) = st in + (* Infix definition for chaining function that accumulate + on a and a ContextObjectSet, ContextObjectMap. *) + let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in + (* This function eases memoization, by checking if an object is already + stored before trying and applying a function. + If the object is there, the function is not fired (we are in a + particular case where memoized object don't need a treatment at all). + If the object isn't there, it is stored and the function is fired*) + let try_and_go o f s m = + if ContextObjectSet.mem o s then + (s,m) + else + f (ContextObjectSet.add o s) m + in + let identity2 s m = (s,m) + in + (* Goes recursively into the term to see if it depends on assumptions. + The 3 important cases are : + - Const _ where we need to first unfold the constant and return + the needed assumptions of its body in the environment, + - Rel _ which means the term is a variable which has been bound + earlier by a Lambda or a Prod (returns [] ), + - Var _ which means that the term refers to a section variable or + a "Let" definition, in the former it is an assumption of [t], + in the latter is must be unfolded like a Const. + The other cases are straightforward recursion. + Calls to the environment are memoized, thus avoiding to explore + the DAG of the environment as if it was a tree (can cause + exponential behavior and prevent the algorithm from terminating + in reasonable time). [s] is a set of [context_object], representing + the object already visited.*) + let rec do_constr t s acc = + let rec iter t = + match kind_of_term t with + | Var id -> do_memoize_id id + | Meta _ | Evar _ -> assert false + | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> + (iter e1)**(iter e2) + | LetIn (_,e1,e2,e3) -> (iter e1)**(iter e2)**(iter e3) + | App (e1, e_array) -> (iter e1)**(iter_array e_array) + | Case (_,e1,e2,e_array) -> (iter e1)**(iter e2)**(iter_array e_array) + | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> + (iter_array e1_array) ** (iter_array e2_array) + | Const kn -> do_memoize_kn kn + | _ -> identity2 (* closed atomic types + rel *) + and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2 + in iter t s acc + + and add_id id s acc = + (* a Var can be either a variable, or a "Let" definition.*) + match Global.lookup_named id with + | (_,None,t) -> + (s,ContextObjectMap.add (Variable id) t acc) + | (_,Some bdy,_) -> do_constr bdy s acc + + and do_memoize_id id = + try_and_go (Variable id) (add_id id) + + and add_kn kn s acc = + let cb = lookup_constant kn in + let do_type cst = + let ctype = + match cb.const_type with + | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) + | NonPolymorphicType t -> t + in + (s,ContextObjectMap.add cst ctype acc) + in + let (s,acc) = + if add_opaque && cb.const_body <> None + && (cb.const_opaque || not (Cpred.mem kn knst)) + then + do_type (Opaque kn) + else (s,acc) + in + match cb.const_body with + | None -> do_type (Axiom kn) + | Some body -> do_constr (Declarations.force body) s acc + + and do_memoize_kn kn = + try_and_go (Axiom kn) (add_kn kn) + + in + fun t -> + snd (do_constr t + (ContextObjectSet.empty) + (ContextObjectMap.empty)) diff --git a/library/assumptions.mli b/library/assumptions.mli new file mode 100644 index 00000000..d0c185d3 --- /dev/null +++ b/library/assumptions.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Term +open Environ + +(** A few declarations for the "Print Assumption" command + @author spiwack *) +type context_object = + | Variable of identifier (** A section variable or a Let definition *) + | Axiom of constant (** An axiom or a constant. *) + | Opaque of constant (** An opaque constant. *) + +(** AssumptionSet.t is a set of [assumption] *) +module OrderedContextObject : Set.OrderedType with type t = context_object +module ContextObjectMap : Map.S with type key = context_object + +(** collects all the assumptions (optionally including opaque definitions) + on which a term relies (together with their type) *) +val assumptions : + ?add_opaque:bool -> transparent_state -> constr -> + Term.types ContextObjectMap.t diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 0bb052be..20690fa8 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_kinds.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: decl_kinds.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Libnames diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 2d31932f..38e83b1e 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_kinds.mli 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: decl_kinds.mli 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Libnames diff --git a/library/declare.ml b/library/declare.ml index 4f5bf2bb..14cddd6c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: declare.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (** This module is about the low-level declaration of logical objects *) diff --git a/library/declare.mli b/library/declare.mli index f2a61180..1ada7cc9 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declare.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: declare.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/library/declaremods.ml b/library/declaremods.ml index ef8f2ddd..7d996a66 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: declaremods.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) open Pp open Util diff --git a/library/declaremods.mli b/library/declaremods.mli index 51455ff6..46b7f411 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: declaremods.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/library/decls.ml b/library/decls.ml index 83d5ea08..425fe798 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decls.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: decls.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (** This module registers tables for some non-logical informations associated declarations *) diff --git a/library/decls.mli b/library/decls.mli index 0bb66fe5..7a8e138b 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: decls.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: decls.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Names open Sign diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index a8ee5e96..2a4d5494 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dischargedhypsmap.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: dischargedhypsmap.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Libnames diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index 77bcf2df..59dcdf24 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dischargedhypsmap.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: dischargedhypsmap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Libnames diff --git a/library/global.ml b/library/global.ml index 5139c252..72429c76 100644 --- a/library/global.ml +++ b/library/global.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: global.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/library/global.mli b/library/global.mli index 4290aaa0..cdcf5801 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: global.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: global.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/library/goptions.ml b/library/goptions.ml index 8cf560d5..178c436d 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: goptions.ml 13922 2011-03-21 16:25:18Z letouzey $ *) +(* $Id: goptions.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* This module manages customization parameters at the vernacular level *) diff --git a/library/goptions.mli b/library/goptions.mli index 2962b5ca..78c4d8e6 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: goptions.mli 13922 2011-03-21 16:25:18Z letouzey $ i*) +(*i $Id: goptions.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* This module manages customization parameters at the vernacular level *) diff --git a/library/heads.ml b/library/heads.ml index 52f98e6d..8244761d 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: heads.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: heads.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util @@ -82,7 +82,9 @@ let kind_of_head env t = match pi2 (lookup_named id env) with | Some c -> aux k l c b | None -> NotImmediatelyComputableHead) - | Const cst -> on_subterm k l b (constant_head cst) + | Const cst -> + (try on_subterm k l b (constant_head cst) + with Not_found -> assert false) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType diff --git a/library/heads.mli b/library/heads.mli index 156b1307..e13b171f 100644 --- a/library/heads.mli +++ b/library/heads.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: heads.mli 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: heads.mli 14641 2011-11-06 11:59:10Z herbelin $ *) open Names open Term diff --git a/library/impargs.ml b/library/impargs.ml index e695be3c..1c2b5afe 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 13499 2010-10-05 10:08:44Z herbelin $ *) +(* $Id: impargs.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/library/impargs.mli b/library/impargs.mli index 0b0ae544..7ec7767b 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: impargs.mli 13499 2010-10-05 10:08:44Z herbelin $ i*) +(*i $Id: impargs.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/library/lib.ml b/library/lib.ml index fde67940..6f8655d3 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: lib.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/library/lib.mli b/library/lib.mli index 3abe22ec..7eb8b688 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: lib.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s This module provides a general mechanism to keep a trace of all operations diff --git a/library/libnames.ml b/library/libnames.ml index d81dc60f..2986940d 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: libnames.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) open Pp open Util diff --git a/library/libnames.mli b/library/libnames.mli index 5dcb61ea..a7bc3b52 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: libnames.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/library/libobject.ml b/library/libobject.ml index 5c7d27c6..7b61a386 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: libobject.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: libobject.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/library/libobject.mli b/library/libobject.mli index 130708aa..c0d89e4d 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libobject.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: libobject.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/library/library.ml b/library/library.ml index c8fd89bf..09f92e6a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: library.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/library/library.mli b/library/library.mli index e835843d..bc939666 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: library.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: library.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/library/library.mllib b/library/library.mllib index 4efb69a2..e8b5a7a4 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -13,4 +13,4 @@ Dischargedhypsmap Goptions Decls Heads - +Assumptions
\ No newline at end of file diff --git a/library/nameops.ml b/library/nameops.ml index fad4f44c..6a4bec5a 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: nameops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/library/nameops.mli b/library/nameops.mli index 91434361..e549d506 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nameops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: nameops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Names diff --git a/library/nametab.ml b/library/nametab.ml index c8d6967c..c4ea5953 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nametab.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: nametab.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Pp diff --git a/library/nametab.mli b/library/nametab.mli index 386f3d55..d0c24bfa 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nametab.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: nametab.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/library/states.ml b/library/states.ml index 5fc26045..679f9028 100644 --- a/library/states.ml +++ b/library/states.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: states.ml 13431 2010-09-18 08:15:29Z herbelin $ *) +(* $Id: states.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open System diff --git a/library/states.mli b/library/states.mli index b6bdff8b..fc6497b6 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: states.mli 13431 2010-09-18 08:15:29Z herbelin $ i*) +(*i $Id: states.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s States of the system. In that module, we provide functions to get and set the state of the whole system. Internally, it is done by diff --git a/library/summary.ml b/library/summary.ml index 376f41d7..a40a9354 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: summary.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: summary.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/library/summary.mli b/library/summary.mli index 00301613..5db9617b 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: summary.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: summary.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) |