Imported Upstream version 8.3.pl3upstream/8.3.pl3

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. *)