Imported Upstream version 8.4~betaupstream/8.4_beta

37 files changed, 991 insertions, 888 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 9ce22b09..adc7f8ed 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -22,6 +22,8 @@ open Term
 open Declarations
 open Mod_subst
 
+let cst_ord k1 k2 = kn_ord (canonical_con k1) (canonical_con k2)
+
 type context_object =
   | Variable of identifier (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
@@ -34,10 +36,8 @@ struct
   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
+      | Axiom k1 , Axiom k2 -> cst_ord k1 k2
+      | Opaque k1 , Opaque k2 -> cst_ord k1 k2
       | Variable _ , Axiom _ -> -1
       | Axiom _ , Variable _ -> 1
       | Opaque _ , _ -> -1
@@ -142,7 +142,7 @@ let lookup_constant_in_impl cst fallback =
 let lookup_constant cst =
   try
     let cb = Global.lookup_constant cst in
-    if cb.const_body <> None then cb
+    if constant_has_body cb then cb
     else lookup_constant_in_impl cst (Some cb)
   with Not_found -> lookup_constant_in_impl cst None
 
@@ -211,20 +211,20 @@ let assumptions ?(add_opaque=false) st (* t *) =
     let cb = lookup_constant kn in
     let do_type cst =
       let ctype =
-	match cb.const_type with
+	match cb.Declarations.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))
+      if add_opaque && Declarations.constant_has_body cb
+	&& (Declarations.is_opaque cb || not (Cpred.mem kn knst))
       then
 	do_type (Opaque kn)
       else (s,acc)
     in
-      match cb.const_body with
+      match Declarations.body_of_constant cb with
       | None -> do_type (Axiom kn)
       | Some body -> do_constr (Declarations.force body) s acc
 
diff --git a/library/assumptions.mli b/library/assumptions.mli
index d0c185d3..1e3e9ef8 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 20690fa8..ba40f98c 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Libnames
 
@@ -17,8 +15,6 @@ type locality =
   | Local
   | Global
 
-type boxed_flag = bool
-
 type theorem_kind =
   | Theorem
   | Lemma
@@ -54,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural
 *)
 type assumption_kind = locality * assumption_object_kind
 
-type definition_kind = locality * boxed_flag * definition_object_kind
+type definition_kind = locality * definition_object_kind
 
 (* Kinds used in proofs *)
 
@@ -86,12 +82,12 @@ let string_of_theorem_kind = function
   | Proposition -> "Proposition"
   | Corollary -> "Corollary"
 
-let string_of_definition_kind (l,boxed,d) =
-  match (l,d) with
+let string_of_definition_kind def =
+  match def with
   | Local, Coercion -> "Coercion Local"
   | Global, Coercion -> "Coercion"
   | Local, Definition -> "Let"
-  | Global, Definition -> if boxed then "Boxed Definition" else "Definition"
+  | Global, Definition -> "Definition"
   | Local, SubClass -> "Local SubClass"
   | Global, SubClass -> "SubClass"
   | Global, CanonicalStructure -> "Canonical Structure"
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 38e83b1e..88ef763c 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -1,24 +1,20 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Libnames
 
-(* Informal mathematical status of declarations *)
+(** Informal mathematical status of declarations *)
 
 type locality =
   | Local
   | Global
 
-type boxed_flag = bool
-
 type theorem_kind =
   | Theorem
   | Lemma
@@ -44,7 +40,7 @@ type definition_object_kind =
 
 type assumption_object_kind = Definitional | Logical | Conjectural
 
-(* [assumption_kind]
+(** [assumption_kind]
 
                 |  Local      | Global
    ------------------------------------
@@ -54,9 +50,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural
 *)
 type assumption_kind = locality * assumption_object_kind
 
-type definition_kind = locality * boxed_flag * definition_object_kind
+type definition_kind = locality * definition_object_kind
 
-(* Kinds used in proofs *)
+(** Kinds used in proofs *)
 
 type goal_object_kind =
   | DefinitionBody of definition_object_kind
@@ -64,31 +60,31 @@ type goal_object_kind =
 
 type goal_kind = locality * goal_object_kind
 
-(* Kinds used in library *)
+(** Kinds used in library *)
 
 type logical_kind =
   | IsAssumption of assumption_object_kind
   | IsDefinition of definition_object_kind
   | IsProof of theorem_kind
 
-(* Utils *)
+(** Utils *)
 
 val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
 val string_of_theorem_kind : theorem_kind -> string
 val string_of_definition_kind :
-  locality * boxed_flag * definition_object_kind -> string
+  locality * definition_object_kind -> string
 
-(* About locality *)
+(** About locality *)
 
 val strength_of_global : global_reference -> locality
 val string_of_strength : locality -> string
 
-(* About recursive power of type declarations *)
+(** About recursive power of type declarations *)
 
 type recursivity_kind =
-  | Finite (* = inductive *)
-  | CoFinite (* = coinductive *)
-  | BiFinite (* = non-recursive, like in "Record" definitions *)
+  | Finite (** = inductive *)
+  | CoFinite (** = coinductive *)
+  | BiFinite (** = non-recursive, like in "Record" definitions *)
 
-(* helper, converts to "finiteness flag" booleans *)
+(** helper, converts to "finiteness flag" booleans *)
 val recursivity_flag_of_kind : recursivity_kind -> bool
diff --git a/library/declare.ml b/library/declare.ml
index 14cddd6c..28858085 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (** This module is about the low-level declaration of logical objects *)
 
 open Pp
@@ -80,7 +78,10 @@ let discharge_variable (_,o) = match o with
   | Inr (id,_) -> Some (Inl (variable_constraints id))
   | Inl _ -> Some o
 
-let (inVariable,_) =
+type variable_obj =
+    (Univ.constraints, identifier * variable_declaration) union
+
+let inVariable : variable_obj -> obj =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
     discharge_function = discharge_variable;
@@ -105,20 +106,26 @@ type constant_declaration = constant_entry * logical_kind
 let load_constant i ((sp,kn),(_,_,kind)) =
   if Nametab.exists_cci sp then
     alreadydeclared (pr_id (basename sp) ++ str " already exists");
-  let con = Global.constant_of_delta (constant_of_kn kn) in
+  let con = Global.constant_of_delta_kn kn in
   Nametab.push (Nametab.Until i) sp (ConstRef con);
   add_constant_kind con kind
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
-  let con = Global.constant_of_delta (constant_of_kn kn) in
+  let con = Global.constant_of_delta_kn kn in
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
+let exists_name id =
+  variable_exists id or Global.exists_label (label_of_id id)
+
+let check_exists sp =
+  let id = basename sp in
+  if exists_name id then alreadydeclared (pr_id id ++ str " already exists")
+
 let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  if variable_exists id or Nametab.exists_cci sp then
-    alreadydeclared (pr_id id ++ str " already exists");
+  check_exists sp;
   let kn' = Global.add_constant dir id cdt in
   assert (kn' = constant_of_kn kn);
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
@@ -141,13 +148,16 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false))
+let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None))
 
 let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let (inConstant,_) =
+type constant_obj =
+    global_declaration * Dischargedhypsmap.discharged_hyps * logical_kind
+
+let inConstant : constant_obj -> obj =
   declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
@@ -156,35 +166,19 @@ let (inConstant,_) =
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
 
-let hcons_constant_declaration = function
-  | DefinitionEntry ce when !Flags.hash_cons_proofs ->
-      let (hcons1_constr,_) = hcons_constr (hcons_names()) in
-      DefinitionEntry
-       { const_entry_body = hcons1_constr ce.const_entry_body;
-	 const_entry_type = Option.map hcons1_constr ce.const_entry_type;
-         const_entry_opaque = ce.const_entry_opaque;
-         const_entry_boxed = ce.const_entry_boxed }
-  | cd -> cd
-
 let declare_constant_common id dhyps (cd,kind) =
   let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in
-  let c = Global.constant_of_delta (constant_of_kn kn) in
+  let c = Global.constant_of_delta_kn kn in
   declare_constant_implicits c;
   Heads.declare_head (EvalConstRef c);
   Notation.declare_ref_arguments_scope (ConstRef c);
   c
 
-let declare_constant_gen internal id (cd,kind) =
-  let cd = hcons_constant_declaration cd in
+let declare_constant ?(internal = UserVerbose) id (cd,kind) =
   let kn = declare_constant_common id [] (ConstantEntry cd,kind) in
   !xml_declare_constant (internal,kn);
   kn
 
-(* TODO: add a third function to distinguish between KernelVerbose
- * and user Verbose *)
-let declare_internal_constant = declare_constant_gen KernelSilent
-let declare_constant = declare_constant_gen UserVerbose
-
 (** Declaration of inductive blocks *)
 
 let declare_inductive_argument_scopes kn mie =
@@ -196,7 +190,7 @@ let declare_inductive_argument_scopes kn mie =
 
 let inductive_names sp kn mie =
   let (dp,_) = repr_path sp in
-  let kn = Global.mind_of_delta (mind_of_kn kn) in
+  let kn = Global.mind_of_delta_kn kn in
   let names, _ =
     List.fold_left
       (fun (names, n) ind ->
@@ -215,16 +209,8 @@ let inductive_names sp kn mie =
       ([], 0) mie.mind_entry_inds
   in names
 
-let check_exists_inductive (sp,_) =
-  (if variable_exists (basename sp) then
-    alreadydeclared (pr_id (basename sp) ++ str " already exists"));
-  if Nametab.exists_cci sp then
-    let (_,id) = repr_path sp in
-    alreadydeclared (pr_id id ++ str " already exists")
-
 let load_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
-  List.iter check_exists_inductive names;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
 
 let open_inductive i ((sp,kn),(_,mie)) =
@@ -233,7 +219,7 @@ let open_inductive i ((sp,kn),(_,mie)) =
 
 let cache_inductive ((sp,kn),(dhyps,mie)) =
   let names = inductive_names sp kn mie in
-  List.iter check_exists_inductive names;
+  List.iter check_exists (List.map fst names);
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   let kn' = Global.add_mind dir id mie in
@@ -245,7 +231,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
 
 
 let discharge_inductive ((sp,kn),(dhyps,mie)) =
-  let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+  let mind = Global.mind_of_delta_kn kn in
   let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
   let sechyps = section_segment_of_mutual_inductive mind in
@@ -266,7 +252,9 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
 
-let (inInductive,_) =
+type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
+
+let inInductive : inductive_obj -> obj =
   declare_object {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
     load_function = load_inductive;
@@ -281,7 +269,7 @@ let declare_mind isrecord mie =
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives" in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
-  let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+  let mind = Global.mind_of_delta_kn kn in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   !xml_declare_inductive (isrecord,oname);
diff --git a/library/declare.mli b/library/declare.mli
index 1ada7cc9..61c19996 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -1,14 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declare.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Libnames
 open Term
@@ -19,9 +16,8 @@ open Indtypes
 open Safe_typing
 open Nametab
 open Decl_kinds
-(*i*)
 
-(* This module provides the official functions to declare new variables,
+(** This module provides the official functions to declare new variables,
    parameters, constants and inductive types. Using the following functions
    will add the entries in the global environment (module [Global]), will
    register the declarations in the library (module [Lib]) --- so that the
@@ -30,54 +26,57 @@ open Decl_kinds
 
 open Nametab
 
-(* Declaration of local constructions (Variable/Hypothesis/Local) *)
+(** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool (* Implicit status *)
+  | SectionLocalDef of constr * types option * bool (** opacity *)
+  | SectionLocalAssum of types * bool (** Implicit status *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
 val declare_variable : variable -> variable_declaration -> object_name
 
-(* Declaration of global constructions *)
-(* i.e. Definition/Theorem/Axiom/Parameter/... *)
+(** Declaration of global constructions 
+   i.e. Definition/Theorem/Axiom/Parameter/... *)
 
 type constant_declaration = constant_entry * logical_kind
 
-(* [declare_constant id cd] declares a global declaration
+(** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
-   the full path of the declaration *)
+   the full path of the declaration 
+
+  internal specify if the constant has been created by the kernel or by the
+  user, and in the former case, if its errors should be silent
+   
+   *)
 type internal_flag =
   | KernelVerbose
   | KernelSilent
   | UserVerbose
 
 val declare_constant :
- identifier -> constant_declaration -> constant
-
-val declare_internal_constant :
-  identifier -> constant_declaration -> constant
+ ?internal:internal_flag -> identifier -> constant_declaration -> constant
 
-(* [declare_mind me] declares a block of inductive types with
+(** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block (boolean must be true iff it is a record) *)
 val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
 
-(* Hooks for XML output *)
+(** Hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
 val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit
 val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit
 
-(* Hook for the cache function of constants and inductives *)
+(** Hook for the cache function of constants and inductives *)
 val add_cache_hook : (full_path -> unit) -> unit
 
-(* Declaration messages *)
+(** Declaration messages *)
 
 val definition_message : identifier -> unit
 val assumption_message : identifier -> unit
 val fixpoint_message : int array option -> identifier list -> unit
 val cofixpoint_message : identifier list -> unit
-val recursive_message : bool (* true = fixpoint *) ->
+val recursive_message : bool (** true = fixpoint *) ->
   int array option -> identifier list -> unit
 
+val exists_name : identifier -> bool
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 7d996a66..90d4245a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Pp
 open Util
 open Names
@@ -19,8 +17,55 @@ open Lib
 open Nametab
 open Mod_subst
 
-(* modules and components *)
+(** Rigid / flexible signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Should we adapt a few scopes during functor application ? *)
+
+type scope_subst = (string * string) list
+
+let scope_subst = ref (Stringmap.empty : string Stringmap.t)
+
+let add_scope_subst sc sc' =
+  scope_subst := Stringmap.add sc sc' !scope_subst
+
+let register_scope_subst scl =
+  List.iter (fun (sc1,sc2) -> add_scope_subst sc1 sc2) scl
+
+let subst_scope sc =
+ try Stringmap.find sc !scope_subst with Not_found -> sc
+
+let reset_scope_subst () =
+  scope_subst := Stringmap.empty
+
+(** Which inline annotations should we honor, either None or the ones
+    whose level is less or equal to the given integer *)
+
+type inline =
+  | NoInline
+  | DefaultInline
+  | InlineAt of int
+
+let default_inline () = Some (Flags.get_inline_level ())
+
+let inl2intopt = function
+  | NoInline -> None
+  | InlineAt i -> Some i
+  | DefaultInline -> default_inline ()
+
+type funct_app_annot =
+  { ann_inline : inline;
+    ann_scope_subst : scope_subst }
 
+let inline_annot a = inl2intopt a.ann_inline
+
+type 'a annotated = ('a * funct_app_annot)
+
+
+(* modules and components *)
 
 (* OBSOLETE This type is a functional closure of substitutive lib_objects.
 
@@ -80,7 +125,8 @@ let modtab_objects =
 let openmod_info =
   ref ((MPfile(initial_dir),[],None,[])
 	 : module_path *  mod_bound_id list *
-           (module_struct_entry * bool) option * module_type_body list)
+           (module_struct_entry * int option) option *
+	   module_type_body list)
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
@@ -133,15 +179,21 @@ let check_sub mtb sub_mtb_l =
    environment. *)
 
 let check_subtypes mp sub_mtb_l =
-  let env = Global.env () in
-  let mb = Environ.lookup_module mp env in
-  let mtb = Modops.module_type_of_module env None mb in
+  let mb =
+    try Global.lookup_module mp
+    with Not_found -> assert false
+  in
+  let mtb = Modops.module_type_of_module None mb in
   check_sub mtb sub_mtb_l
 
 (* Same for module type [mp] *)
 
 let check_subtypes_mt mp sub_mtb_l =
-  check_sub (Environ.lookup_modtype mp (Global.env())) sub_mtb_l
+  let mtb =
+    try Global.lookup_modtype mp
+    with Not_found -> assert false
+  in
+  check_sub mtb sub_mtb_l
 
 (* Create a functor type entry *)
 
@@ -154,7 +206,8 @@ let funct_entry args m =
 
 let build_subtypes interp_modtype mp args mtys =
   List.map
-    (fun (m,inl) ->
+    (fun (m,ann) ->
+       let inl = inline_annot ann in
        let mte = interp_modtype (Global.env()) m in
        let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in
        let funct_mtb =
@@ -228,43 +281,27 @@ let conv_names_do_module exists what iter_objects i
    functions can be called only once (and "end_mod*" set the flag to
    false then)
 *)
-let cache_module ((sp,kn),(entry,substobjs)) =
+let cache_module ((sp,kn),substobjs) =
   let dir,mp = dir_of_sp sp, mp_of_kn kn in
     do_module false "cache" load_objects 1 dir mp substobjs []
-    
-(* TODO: This check is not essential *)
-let check_empty s = function
-     | None -> ()
-     | Some _ ->
-	 anomaly ("We should never have full info in " ^ s^"!")
-
 
 (* When this function is called the module itself is already in the
    environment. This function loads its objects only *)
 
-let load_module i (oname,(entry,substobjs)) =
-  (* TODO: This check is not essential *)
-  check_empty "load_module" entry;
+let load_module i (oname,substobjs) =
   conv_names_do_module false "load" load_objects i oname substobjs
 
-
-let open_module i (oname,(entry,substobjs)) =
-  (* TODO: This check is not essential *)
-  check_empty "open_module" entry;
+let open_module i (oname,substobjs) =
   conv_names_do_module true "open" open_objects i oname substobjs
 
+let subst_module (subst,(mbids,mp,objs)) =
+  (mbids,subst_mp subst mp, subst_objects subst objs)
 
+let classify_module substobjs = Substitute substobjs
 
-let subst_module (subst,(entry,(mbids,mp,objs))) =
-  check_empty "subst_module" entry;
-    (None,(mbids,subst_mp subst mp, subst_objects subst objs))
-
-
-let classify_module (_,substobjs) =
-  Substitute (None,substobjs)
-
-let (in_module,out_module) =
-  declare_object {(default_object "MODULE") with
+let (in_module : substitutive_objects -> obj),
+    (out_module : obj -> substitutive_objects) =
+  declare_object_full {(default_object "MODULE") with
     cache_function = cache_module;
     load_function = load_module;
     open_function = open_module;
@@ -291,7 +328,7 @@ let open_keep i ((sp,kn),seg) =
   let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
     open_objects i (dirpath,(mp,empty_dirpath)) seg
 
-let (in_modkeep,_) =
+let in_modkeep : lib_objects -> obj =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
     cache_function = cache_keep;
     load_function = load_keep;
@@ -323,6 +360,7 @@ let _ = Summary.declare_summary "MODTYPE-INFO"
 let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
   let mp = mp_of_kn kn in
 
+  (* We enrich the global environment *)
   let _ =
     match entry with
       | None ->
@@ -346,7 +384,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
 
 
 let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
-  check_empty "load_modtype" entry;
+  assert (entry = None);
 
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
@@ -358,7 +396,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
 
 
 let open_modtype i ((sp,kn),(entry,_,_)) =
-  check_empty "open_modtype" entry;
+  assert (entry = None);
 
   if
     try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn)
@@ -370,15 +408,18 @@ let open_modtype i ((sp,kn),(entry,_,_)) =
   Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
 
 let subst_modtype (subst,(entry,(mbids,mp,objs),_)) =
-  check_empty "subst_modtype" entry;
+  assert (entry = None);
   (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[])
 
-
 let classify_modtype (_,substobjs,_) =
   Substitute (None,substobjs,[])
 
+type modtype_obj =
+    (module_struct_entry * Entries.inline) option (* will be None in vo *)
+    * substitutive_objects
+    * module_type_body list
 
-let (in_modtype,_) =
+let in_modtype : modtype_obj -> obj =
     declare_object {(default_object "MODULE TYPE") with
       cache_function = cache_modtype;
       open_function = open_modtype;
@@ -386,36 +427,27 @@ let (in_modtype,_) =
       subst_function = subst_modtype;
       classify_function = classify_modtype }
 
+let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
+  if mbids<>[] then anomaly "Unexpected functor objects";
+  let rec replace_idl = function
+    | _,[] -> []
+    | id::idl,(id',obj)::tail when id = id' ->
+      if object_tag obj <> "MODULE" then anomaly "MODULE expected!";
+      let substobjs =
+	if idl = [] then
+	  let mp' = MPdot(mp, label_of_id id) in
+	  mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs
+	else
+	  replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp
+      in
+      (id, in_module substobjs)::tail
+    | idl,lobj::tail -> lobj::replace_idl (idl,tail)
+  in
+  (mbids, mp, replace_idl (idl,lib_stack))
 
-let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1=
-  if mbids<>[] then 
-    error "Unexpected functor objects"
-  else
-    let rec replace_idl = function 
-      | _,[] -> [] 
-      | id::idl,(id',obj)::tail when id = id' ->
-	  if object_tag obj = "MODULE" then
-           (match idl with
-               [] -> (id, in_module 
-			(None,(mbids,(MPdot(mp,label_of_id id)),subst_objects 
-				 (map_mp mp1 (MPdot(mp,label_of_id id)) empty_delta_resolver) objs)))::tail
-             | _ ->
-               let (_,substobjs) = out_module obj in
-                let substobjs' = replace_module_object idl substobjs 
-		  (mbids2,mp2,objs) mp in
-                  (id, in_module (None,substobjs'))::tail
-           )
-	  else error "MODULE expected!"
-      | idl,lobj::tail -> lobj::replace_idl (idl,tail)
-    in
-      (mbids, mp, replace_idl (idl,lib_stack))
-
-let discr_resolver mb  = 
-     match mb.mod_type with
-	SEBstruct _ -> 
-	  Some mb.mod_delta
-      | _ -> (*case mp is a functor *)
-	  None
+let discr_resolver mb = match mb.mod_type with
+  | SEBstruct _ -> Some mb.mod_delta
+  | _ -> None (* when mp is a functor *)
 
 (* Small function to avoid module typing during substobjs retrivial  *)
 let rec get_objs_modtype_application env = function
@@ -428,24 +460,20 @@ let rec get_objs_modtype_application env = function
     Modops.error_application_to_not_path mexpr
 | _ -> error "Application of a non-functor."
 
-let rec compute_subst env mbids sign mp_l inline =
+let rec compute_subst env mbids sign mp_l inl =
   match mbids,mp_l with
     | _,[] -> mbids,empty_subst
     | [],r -> error "Application of a functor with too few arguments."
     | mbid::mbids,mp::mp_l ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
 	let mb = Environ.lookup_module mp env in
-	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inline in
-	match discr_resolver mb with
-	  | None ->
-	      mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst
+	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
+	let resolver = match discr_resolver mb with
+	  | None -> empty_delta_resolver
 	  | Some mp_delta ->
-	      let mp_delta =
-		if not inline then mp_delta else
-		  Modops.complete_inline_delta_resolver env mp
-		    farg_id farg_b mp_delta
-	      in
-	      mbid_left,join (map_mbid mbid mp mp_delta) subst
+	      Modops.inline_delta_resolver env inl mp farg_id farg_b mp_delta
+	in
+	mbid_left,join (map_mbid mbid mp resolver) subst
 
 let rec get_modtype_substobjs env mp_from inline = function
     MSEident ln -> 
@@ -472,20 +500,39 @@ let rec get_modtype_substobjs env mp_from inline = function
 (* push names of bound modules (and their components) to Nametab *)
 (* add objects associated to them *)
 let process_module_bindings argids args =
-  let process_arg id (mbid,(mty,inl)) =
+  let process_arg id (mbid,(mty,ann)) =
     let dir = make_dirpath [id] in
     let mp = MPbound mbid in
     let (mbids,mp_from,objs) =
-      get_modtype_substobjs (Global.env()) mp inl mty in
+      get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty in
     let substobjs = (mbids,mp,subst_objects
 		       (map_mp mp_from mp empty_delta_resolver) objs)in
       do_module false "start" load_objects 1 dir mp substobjs []
     in
       List.iter2 process_arg argids args
 
-let intern_args interp_modtype (idl,(arg,inl)) =
+(* Same with module_type_body *)
+
+let rec seb2mse = function
+  | SEBident mp -> MSEident mp
+  | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s')
+  | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp))
+  | SEBwith (s,With_definition_body(l,cb)) ->
+      (match cb.const_body with
+	| Def c -> MSEwith(seb2mse s,With_Definition(l,Declarations.force c))
+	| _ -> assert false)
+  | _ -> failwith "seb2mse: received a non-atomic seb"
+
+let process_module_seb_binding mbid seb =
+  process_module_bindings [id_of_mbid mbid]
+    [mbid,
+     (seb2mse seb,
+      { ann_inline = DefaultInline; ann_scope_subst = [] })]
+
+let intern_args interp_modtype (idl,(arg,ann)) =
+  let inl = inline_annot ann in
   let lib_dir = Lib.library_dp() in
-  let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
+  let mbids = List.map (fun (_,id) -> make_mbid lib_dir id) idl in
   let mty = interp_modtype (Global.env()) arg in
   let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
   let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
@@ -504,11 +551,12 @@ let start_module_ interp_modtype export id args res fs =
   let mp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
   let res_entry_o, sub_body_l = match res with
-    | Topconstr.Enforce (res,inl) ->
+    | Enforce (res,ann) ->
+        let inl = inline_annot ann in
 	let mte = interp_modtype (Global.env()) res in
 	let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in
 	Some (mte,inl), []
-    | Topconstr.Check resl ->
+    | Check resl ->
 	None, build_subtypes interp_modtype mp arg_entries resl
   in
   let mbids = List.map fst arg_entries in
@@ -561,7 +609,7 @@ let end_module () =
     | Some mp_from,(mbids,_,objs) ->
 	(mbids,mp,subst_objects (map_mp mp_from mp resolver) objs) 
   in
-  let node = in_module (None,substobjs) in
+  let node = in_module substobjs in
   let objects =
     if keep = [] || mbids <> [] then
       special@[node]   (* no keep objects or we are defining a functor *)
@@ -652,7 +700,7 @@ let subst_import (subst,(export,mp as obj)) =
     if mp'==mp then obj else
       (export,mp')
 
-let (in_import,_) =
+let in_import =
   declare_object {(default_object "IMPORT MODULE") with
 		    cache_function = cache_import;
 		    open_function = (fun i o -> if i=1 then cache_import o);
@@ -698,7 +746,8 @@ let end_modtype () =
   mp
 
 
-let declare_modtype_ interp_modtype id args mtys (mty,inl) fs =
+let declare_modtype_ interp_modtype id args mtys (mty,ann) fs =
+  let inl = inline_annot ann in
   let mmp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
   let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in
@@ -708,9 +757,11 @@ let declare_modtype_ interp_modtype id args mtys (mty,inl) fs =
   (* Undo the simulated interactive building of the module type *)
   (* and declare the module type as a whole *)
 
+  register_scope_subst ann.ann_scope_subst;
   let substobjs = (mbids,mmp,
 		   subst_objects (map_mp mp_from mmp empty_delta_resolver) objs)
   in
+  reset_scope_subst ();
   Summary.unfreeze_summaries fs;
   ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l)));
   mmp
@@ -744,6 +795,60 @@ let rec get_module_substobjs env mp_from inl = function
   | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from inl mty
   | MSEwith (mty, With_Module (idl,mp)) -> assert false
 
+
+let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
+  let mmp = Global.start_module id in
+  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
+
+  let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
+  let env = Global.env() in
+  let mty_entry_o, subs, inl_res = match res with
+    | Enforce (mty,ann) ->
+        Some (funct interp_modtype mty), [], inline_annot ann
+    | Check mtys ->
+	None, build_subtypes interp_modtype mmp arg_entries mtys,
+        default_inline ()
+  in
+ 
+  (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
+  let mexpr_entry_o, inl_expr, scl = match mexpr_o with
+    | None -> None, default_inline (), []
+    | Some (mexpr,ann) ->
+      Some (funct interp_modexpr mexpr), inline_annot ann, ann.ann_scope_subst
+
+  in
+  let entry =
+    {mod_entry_type = mty_entry_o;
+     mod_entry_expr = mexpr_entry_o }
+  in
+
+  let substobjs =
+    match entry with
+      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
+      | _ -> anomaly "declare_module: No type, no body ..."
+  in
+  let (mbids,mp_from,objs) = substobjs in
+  (* Undo the simulated interactive building of the module *)
+  (* and declare the module as a whole *)
+  Summary.unfreeze_summaries fs;
+  let mp = mp_of_kn (Lib.make_kn id) in
+  let inl = if inl_expr = None then None else inl_res in (*PLTODO *)
+  let mp_env,resolver = Global.add_module id entry inl in
+
+  if mp_env <> mp then anomaly "Kernel and Library names do not match";
+
+  
+  check_subtypes mp subs;
+  register_scope_subst scl;
+  let substobjs = (mbids,mp_env,
+		   subst_objects(map_mp mp_from mp_env resolver) objs) in
+  reset_scope_subst ();
+  ignore (add_leaf
+	    id
+	    (in_module substobjs));
+  mmp
+
 (* Include *)
 
 let rec subst_inc_expr subst me =
@@ -769,95 +874,48 @@ let lift_oname (sp,kn) =
   let dir,_ = Libnames.repr_path sp in
     (dir,mp)
 
-let cache_include (oname,((me,is_mod),(mbis,mp1,objs))) =
+let cache_include (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
     load_objects 1 prefix objs;
-    open_objects 1 prefix objs 
-    
-let load_include  i (oname,((me,is_mod),(mbis,mp1,objs))) =
+    open_objects 1 prefix objs
+
+let load_include  i (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
     load_objects i prefix objs
-      
-      
-let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) =
+
+let open_include i (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
     open_objects i prefix objs
-      
-let subst_include (subst,((me,is_mod),substobj)) =
+
+let subst_include (subst,(me,substobj)) =
   let (mbids,mp,objs) = substobj in
   let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in
-    ((subst_inc_expr subst me,is_mod),substobjs)
-      
-let classify_include ((me,is_mod),substobjs) =
-  Substitute ((me,is_mod),substobjs)
+    (subst_inc_expr subst me,substobjs)
+
+let classify_include (me,substobjs) = Substitute (me,substobjs)
 
-let (in_include,out_include) =
-  declare_object {(default_object "INCLUDE") with
+type include_obj = module_struct_entry * substitutive_objects
+
+let (in_include : include_obj -> obj),
+    (out_include : obj -> include_obj) =
+  declare_object_full {(default_object "INCLUDE") with
     cache_function = cache_include;
     load_function = load_include;
     open_function = open_include;
     subst_function = subst_include;
     classify_function = classify_include }
 
-
-let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
-  let mmp = Global.start_module id in
-  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
-  let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
-  let env = Global.env() in
-  let mty_entry_o, subs, inl_res = match res with
-    | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl
-    | Topconstr.Check mtys ->
-	None, build_subtypes interp_modtype mmp arg_entries mtys, true
-  in
- 
-  (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
-  let mexpr_entry_o, inl_expr = match mexpr_o with
-    | None -> None, true
-    | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
-  in
-  let entry =
-    {mod_entry_type = mty_entry_o;
-     mod_entry_expr = mexpr_entry_o }
-  in
-
-  let(mbids,mp_from,objs) =
-    match entry with
-      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
-      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
-      | _ -> anomaly "declare_module: No type, no body ..."
-  in
-  (* Undo the simulated interactive building of the module *)
-  (* and declare the module as a whole *)
-  Summary.unfreeze_summaries fs;
-  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
-  let mp_env,resolver = Global.add_module id entry (inl_expr&&inl_res) in
-
-  if mp_env <> mp then anomaly "Kernel and Library names do not match";
-
-  
-  check_subtypes mp subs;
-
-  let substobjs = (mbids,mp_env,
-		   subst_objects(map_mp mp_from mp_env resolver) objs) in
-  ignore (add_leaf
-	    id
-	    (in_module (Some (entry), substobjs)));
-  mmp
-
-
 let rec include_subst env mb mbids sign inline =
   match mbids with
     | [] -> empty_subst
     | mbid::mbids ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
 	let subst = include_subst env mb mbids fbody_b inline in
-	let mp_delta = if not inline then mb.mod_delta else
-	  Modops.complete_inline_delta_resolver env mb.mod_mp
+	let mp_delta =
+	  Modops.inline_delta_resolver env inline mb.mod_mp
 	    farg_id farg_b mb.mod_delta
 	in
 	join (map_mbid mbid mb.mod_mp mp_delta) subst
@@ -894,9 +952,13 @@ let get_includeself_substobjs env objs me is_mod inline =
     ([],mp_self,subst_objects subst objects)
   with NothingToDo -> objs
 
-let declare_one_include_inner inl (me,is_mod) =
+
+
+
+let declare_one_include_inner annot (me,is_mod) =
   let env = Global.env() in
   let mp1,_ = current_prefix () in
+  let inl = inline_annot annot in
   let (mbids,mp,objs)=
     if is_mod then
       get_module_substobjs env mp1 inl me
@@ -909,14 +971,15 @@ let declare_one_include_inner inl (me,is_mod) =
       (mbids,mp,objs) in
   let id = current_mod_id() in
   let resolver =  Global.add_include me is_mod inl in
+  register_scope_subst annot.ann_scope_subst;
   let substobjs = (mbids,mp1,
 		   subst_objects (map_mp mp mp1 resolver) objs) in
-  ignore (add_leaf id
-	    (in_include ((me,is_mod), substobjs)))
+  reset_scope_subst ();
+  ignore (add_leaf id (in_include (me, substobjs)))
 
-let declare_one_include interp_struct me_ast =
-  declare_one_include_inner (snd me_ast)
-    (interp_struct (Global.env()) (fst me_ast))
+let declare_one_include interp_struct (me_ast,annot) =
+  declare_one_include_inner annot
+    (interp_struct (Global.env()) me_ast)
 
 let declare_include_ interp_struct me_asts =
   List.iter (declare_one_include interp_struct) me_asts
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 46b7f411..9d44ba97 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -1,14 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Util
 open Names
 open Entries
@@ -16,15 +13,41 @@ open Environ
 open Libnames
 open Libobject
 open Lib
-   (*i*)
 
-(*s This modules provides official functions to declare modules and
+(** This modules provides official functions to declare modules and
   module types *)
 
+(** Rigid / flexible signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Should we adapt a few scopes during functor application ? *)
+
+type scope_subst = (string * string) list
+
+val subst_scope : string -> string
+
+(** Which inline annotations should we honor, either None or the ones
+   whose level is less or equal to the given integer *)
 
-(*s Modules *)
+type inline =
+  | NoInline
+  | DefaultInline
+  | InlineAt of int
 
-(* [declare_module interp_modtype interp_modexpr id fargs typ expr]
+(** The type of annotations for functor applications *)
+
+type funct_app_annot =
+  { ann_inline : inline;
+    ann_scope_subst : scope_subst }
+
+type 'a annotated = ('a * funct_app_annot)
+
+(** {6 Modules } *)
+
+(** [declare_module interp_modtype interp_modexpr id fargs typ expr]
    declares module [id], with type constructed by [interp_modtype]
    from functor arguments [fargs] and [typ] and with module body
    constructed by [interp_modtype] from functor arguments [fargs] and
@@ -41,39 +64,44 @@ val declare_module :
   (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
   identifier ->
-  (identifier located list * ('modast * bool)) list ->
-  ('modast * bool) Topconstr.module_signature ->
-  ('modast * bool) list -> module_path
+  (identifier located list * ('modast annotated)) list ->
+  ('modast annotated) module_signature ->
+  ('modast annotated) list -> module_path
 
 val start_module : (env -> 'modast -> module_struct_entry) ->
-  bool option -> identifier -> (identifier located list * ('modast * bool)) list ->
-  ('modast * bool) Topconstr.module_signature -> module_path
+  bool option -> identifier ->
+  (identifier located list * ('modast annotated)) list ->
+  ('modast annotated) module_signature -> module_path
 
 val end_module : unit -> module_path
 
 
 
-(*s Module types *)
+(** {6 Module types } *)
 
 val declare_modtype : (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
-  identifier -> (identifier located list * ('modast * bool)) list ->
-  ('modast * bool) list -> ('modast * bool) list -> module_path
+  identifier ->
+  (identifier located list * ('modast annotated)) list ->
+  ('modast annotated) list ->
+  ('modast annotated) list ->
+  module_path
 
 val start_modtype : (env -> 'modast -> module_struct_entry) ->
-  identifier -> (identifier located list * ('modast * bool)) list ->
-  ('modast * bool) list -> module_path
+  identifier -> (identifier located list * ('modast annotated)) list ->
+  ('modast annotated) list -> module_path
 
 val end_modtype : unit -> module_path
 
 
-(*s Objects of a module. They come in two lists: the substitutive ones
+(** {6 ... } *)
+(** Objects of a module. They come in two lists: the substitutive ones
   and the other *)
 
 val module_objects : module_path -> library_segment
 
 
-(*s Libraries i.e. modules on disk *)
+(** {6 Libraries i.e. modules on disk } *)
 
 type library_name = dir_path
 
@@ -88,27 +116,28 @@ val start_library : library_name -> unit
 val end_library :
   library_name -> Safe_typing.compiled_library * library_objects
 
-(* set a function to be executed at end_library *)
+(** set a function to be executed at end_library *)
 val set_end_library_hook : (unit -> unit) -> unit
 
-(* [really_import_module mp] opens the module [mp] (in a Caml sense).
+(** [really_import_module mp] opens the module [mp] (in a Caml sense).
    It modifies Nametab and performs the [open_object] function for
    every object of the module. *)
 
 val really_import_module : module_path -> unit
 
-(* [import_module export mp] is a synchronous version of
+(** [import_module export mp] is a synchronous version of
    [really_import_module]. If [export] is [true], the module is also
    opened every time the module containing it is. *)
 
 val import_module : bool -> module_path -> unit
 
-(* Include  *)
+(** Include  *)
 
 val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
-  ('struct_expr * bool) list -> unit
+  ('struct_expr annotated) list -> unit
 
-(*s [iter_all_segments] iterate over all segments, the modules'
+(** {6 ... } *)
+(** [iter_all_segments] iterate over all segments, the modules'
     segments first and then the current segment. Modules are presented
     in an arbitrary order. The given function is applied to all leaves
     (together with their section path). *)
@@ -120,7 +149,10 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
 
 (*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*)
 
-(* For translator *)
+(** For translator *)
 val process_module_bindings : module_ident list ->
-  (mod_bound_id * (module_struct_entry * bool)) list -> unit
+  (mod_bound_id * (module_struct_entry annotated)) list -> unit
 
+(** For Printer *)
+val process_module_seb_binding :
+  mod_bound_id -> Declarations.struct_expr_body -> unit
diff --git a/library/decls.ml b/library/decls.ml
index 425fe798..74a5f7ef 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decls.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (** This module registers tables for some non-logical informations
      associated declarations *)
 
@@ -57,7 +55,8 @@ let constant_kind kn = Cmap.find kn !csttab
 
 (** Miscellaneous functions. *)
 
-let clear_proofs sign =
+let initialize_named_context_for_proof () =
+  let sign = Global.named_context () in
   List.fold_right
     (fun (id,c,t as d) signv ->
       let d = if variable_opacity id then (id,None,t) else d in
diff --git a/library/decls.mli b/library/decls.mli
index 7a8e138b..73f1745b 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: decls.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Names
 open Sign
 open Libnames
@@ -20,7 +18,7 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-    dir_path * bool (* opacity *) * Univ.constraints * logical_kind
+    dir_path * bool (** opacity *) * Univ.constraints * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> dir_path
@@ -35,7 +33,11 @@ val variable_exists : variable -> bool
 val add_constant_kind : constant -> logical_kind -> unit
 val constant_kind : constant -> logical_kind
 
+(* Prepare global named context for proof session: remove proofs of
+   opaque section definitions and remove vm-compiled code *)
+
+val initialize_named_context_for_proof : unit -> Environ.named_context_val
+
 (** Miscellaneous functions *)
 
 val last_section_hyps : dir_path -> identifier list
-val clear_proofs : named_context -> Environ.named_context_val
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 2a4d5494..ec92f679 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dischargedhypsmap.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Libnames
 open Names
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index 59dcdf24..fda071a7 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -1,24 +1,20 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: dischargedhypsmap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Libnames
 open Term
 open Environ
 open Nametab
-(*i*)
 
 type discharged_hyps = full_path list
 
-(*s Discharged hypothesis. Here we store the discharged hypothesis of each *)
-(*  constant or inductive type declaration.                                *)
+(** Discharged hypothesis. Here we store the discharged hypothesis of each 
+    constant or inductive type declaration.                                *)
 
 val set_discharged_hyps : full_path -> discharged_hyps -> unit
 val get_discharged_hyps : full_path -> discharged_hyps
diff --git a/library/global.ml b/library/global.ml
index 72429c76..ab70bb7c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: global.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Names
 open Term
@@ -121,16 +119,22 @@ let lookup_mind kn = lookup_mind kn (env())
 let lookup_module mp = lookup_module mp (env())
 let lookup_modtype kn = lookup_modtype kn (env())
 
-let constant_of_delta con = 
+let constant_of_delta_kn kn =
   let resolver,resolver_param = (delta_of_senv !global_env) in
+  (* TODO : are resolver and resolver_param orthogonal ?
+     the effect of resolver is lost if resolver_param isn't
+     trivial at that spot. *)
     Mod_subst.constant_of_delta resolver_param
-      (Mod_subst.constant_of_delta resolver con)
+      (Mod_subst.constant_of_delta_kn resolver kn)
 
-let mind_of_delta mind = 
+let mind_of_delta_kn kn =
   let resolver,resolver_param = (delta_of_senv !global_env) in
+  (* TODO idem *)
     Mod_subst.mind_of_delta resolver_param
-      (Mod_subst.mind_of_delta resolver mind)
-	
+      (Mod_subst.mind_of_delta_kn resolver kn)
+
+let exists_label id = exists_label id !global_env
+
 let start_library dir =
   let mp,newenv = start_library dir !global_env in
     global_env := newenv;
diff --git a/library/global.mli b/library/global.mli
index cdcf5801..1a0fabdc 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -1,14 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: global.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Univ
 open Term
@@ -17,9 +14,8 @@ open Entries
 open Indtypes
 open Mod_subst
 open Safe_typing
-   (*i*)
 
-(* This module defines the global environment of Coq.  The functions
+(** This module defines the global environment of Coq.  The functions
    below are exactly the same as the ones in [Safe_typing], operating on
    that global environment. [add_*] functions perform name verification,
    i.e. check that the name given as argument match those provided by
@@ -38,11 +34,12 @@ val named_context : unit -> Sign.named_context
 
 val env_is_empty : unit -> bool
 
-(*s Extending env with variables and local definitions *)
+(** {6 Extending env with variables and local definitions } *)
 val push_named_assum : (identifier * types) -> Univ.constraints
 val push_named_def   : (identifier * constr * types option) -> Univ.constraints
 
-(*s Adding constants, inductives, modules and module types.  All these
+(** {6 ... } *)
+(** Adding constants, inductives, modules and module types.  All these
   functions verify that given names match those generated by kernel *)
 
 val add_constant :
@@ -51,57 +48,59 @@ val add_mind        :
   dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive
 
 val add_module      :
- identifier -> module_entry -> bool -> module_path * delta_resolver
+ identifier -> module_entry -> inline -> module_path * delta_resolver
 val add_modtype     :
- identifier -> module_struct_entry -> bool -> module_path
+ identifier -> module_struct_entry -> inline -> module_path
 val add_include :
- module_struct_entry -> bool -> bool -> delta_resolver
+ module_struct_entry -> bool -> inline -> delta_resolver
 
 val add_constraints : constraints -> unit
 
 val set_engagement : engagement -> unit
 
-(*s Interactive modules and module types *)
-(* Both [start_*] functions take the [dir_path] argument to create a
+(** {6 Interactive modules and module types }
+   Both [start_*] functions take the [dir_path] argument to create a
    [mod_self_id]. This should be the name of the compilation unit. *)
 
-(* [start_*] functions return the [module_path] valid for components
+(** [start_*] functions return the [module_path] valid for components
    of the started module / module type *)
 
 val start_module : identifier -> module_path
 
 val end_module : Summary.frozen ->identifier ->
-  (module_struct_entry * bool) option -> module_path * delta_resolver
+  (module_struct_entry * inline) option -> module_path * delta_resolver
 
 val add_module_parameter :
- mod_bound_id -> module_struct_entry -> bool -> delta_resolver
+ mod_bound_id -> module_struct_entry -> inline -> delta_resolver
 
 val start_modtype : identifier -> module_path
 val end_modtype : Summary.frozen -> identifier -> module_path
 val pack_module : unit -> module_body
 
 
-(* Queries *)
+(** Queries *)
 val lookup_named     : variable -> named_declaration
 val lookup_constant  : constant -> constant_body
 val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
 val lookup_mind      : mutual_inductive -> mutual_inductive_body
 val lookup_module    : module_path -> module_body
 val lookup_modtype   : module_path -> module_type_body
-val constant_of_delta : constant -> constant
-val mind_of_delta : mutual_inductive -> mutual_inductive
+val constant_of_delta_kn : kernel_name -> constant
+val mind_of_delta_kn : kernel_name -> mutual_inductive
+val exists_label     : label -> bool
 
-(* Compiled modules *)
+(** Compiled modules *)
 val start_library : dir_path -> module_path
 val export : dir_path -> module_path * compiled_library
 val import : compiled_library -> Digest.t -> module_path
 
-(*s Function to get an environment from the constants part of the global
+(** {6 ... } *)
+(** Function to get an environment from the constants part of the global
  * environment and a given context. *)
 
 val type_of_global : Libnames.global_reference -> types
 val env_of_context : Environ.named_context_val -> Environ.env
 
 
-(* spiwack: register/unregister function for retroknowledge *)
+(** spiwack: register/unregister function for retroknowledge *)
 val register : Retroknowledge.field -> constr -> constr -> unit
diff --git a/library/goptions.ml b/library/goptions.ml
index 178c436d..90c8728c 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* This module manages customization parameters at the vernacular level     *)
 
 open Pp
@@ -19,22 +17,18 @@ open Term
 open Nametab
 open Mod_subst
 
+open Goptionstyp
+
+type option_name = Goptionstyp.option_name
+
 (****************************************************************************)
 (* 0- Common things                                                         *)
 
-type option_name = string list
-
 let nickname table = String.concat " " table
 
 let error_undeclared_key key =
   error ((nickname key)^": no table or option of this type")
 
-type value =
-  | BoolValue   of bool
-  | IntValue    of int option
-  | StringValue of string
-  | IdentValue  of global_reference
-
 (****************************************************************************)
 (* 1- Tables                                                                *)
 
@@ -96,7 +90,7 @@ module MakeTable =
 	    if p' == p then obj else
 	      (f,p')
 	in
-        let (inGo,outGo) =
+        let inGo : option_mark * A.t -> obj =
           Libobject.declare_object {(Libobject.default_object nick) with
                 Libobject.load_function = load_options;
 		Libobject.open_function = load_options;
@@ -201,12 +195,13 @@ module MakeRefTable =
 
 type 'a option_sig = {
   optsync  : bool;
+  optdepr  : bool;
   optname  : string;
   optkey   : option_name;
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
 
-type option_type = bool * (unit -> value) -> (value -> unit)
+type option_type = bool * (unit -> option_value) -> (option_value -> unit)
 
 module OptionMap =
   Map.Make (struct  type t = option_name let compare = compare end)
@@ -230,25 +225,25 @@ open Libobject
 open Lib
 
 let declare_option cast uncast
-  { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } =
+  { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
   (* spiwack: I use two spaces in the nicknames of "local" and "global" objects.
       That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are
        lists of strings *without* spaces. *)
   let (write,lwrite,gwrite) = if sync then
-    let (ldecl_obj,_) = (* "Local": doesn't survive section or modules. *)
+    let ldecl_obj = (* "Local": doesn't survive section or modules. *)
       declare_object {(default_object ("L  "^nickname key)) with
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun _ -> Dispose)}
     in
-    let (decl_obj,_) = (* default locality: survives sections but not modules. *)
+    let decl_obj = (* default locality: survives sections but not modules. *)
       declare_object {(default_object (nickname key)) with
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun _ -> Dispose);
 		       discharge_function = (fun (_,v) -> Some v)}
     in
-    let (gdecl_obj,_) = (* "Global": survives section and modules. *)
+    let gdecl_obj = (* "Global": survives section and modules. *)
       declare_object {(default_object ("G  "^nickname key)) with
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun v -> Substitute v);
@@ -269,7 +264,7 @@ let declare_option cast uncast
   let cwrite v = write (uncast v) in
   let clwrite v = lwrite (uncast v) in
   let cgwrite v = gwrite (uncast v) in
-  value_tab := OptionMap.add key (name,(sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
+  value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
   write
 
 type 'a write_function = 'a -> unit
@@ -292,7 +287,7 @@ let declare_string_option =
 (* Setting values of options *)
 
 let set_option_value locality check_and_cast key v =
-  let (name,(_,read,write,lwrite,gwrite)) =
+  let (name, depr, (_,read,write,lwrite,gwrite)) =
     try get_option key
     with Not_found -> error ("There is no option "^(nickname key)^".")
   in
@@ -330,12 +325,12 @@ let set_int_option_value_gen locality =
   set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
   try set_option_value locality check_bool_value key v
-  with UserError (_,s) -> Flags.if_verbose msg_warning s
+  with UserError (_,s) -> Flags.if_warn msg_warning s
 let set_string_option_value_gen locality =
   set_option_value locality check_string_value
 let unset_option_value_gen locality key =
   try set_option_value locality check_unset_value key ()
-  with UserError (_,s) -> Flags.if_verbose msg_warning s
+  with UserError (_,s) -> Flags.if_warn msg_warning s
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None
@@ -350,10 +345,10 @@ let msg_option_value (name,v) =
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
-    | IdentValue r    -> pr_global_env Idset.empty r
+(*     | IdentValue r    -> pr_global_env Idset.empty r *)
 
 let print_option_value key =
-  let (name,(_,read,_,_,_)) = get_option key in
+  let (name, depr, (_,read,_,_,_)) = get_option key in
   let s = read () in
   match s with
     | BoolValue b ->
@@ -364,25 +359,37 @@ let print_option_value key =
 	     msg_option_value (name,s) ++ fnl ())
 
 
+let get_tables () =
+  let tables = !value_tab in
+  let fold key (name, depr, (sync,read,_,_,_)) accu =
+    let state = {
+      opt_sync = sync;
+      opt_name = name;
+      opt_depr = depr;
+      opt_value = read ();
+    } in
+    OptionMap.add key state accu
+  in
+  OptionMap.fold fold tables OptionMap.empty
+
 let print_tables () =
+  let print_option key name value depr =
+    let msg = str ("  "^(nickname key)^": ") ++ msg_option_value (name, value) in
+    if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
+    else msg ++ fnl ()
+  in
   msg
     (str "Synchronous options:" ++ fnl () ++
      OptionMap.fold
-       (fun key (name,(sync,read,_,_,_)) p ->
-	  if sync then
-	    p ++ str ("  "^(nickname key)^": ") ++
-	    msg_option_value (name,read()) ++ fnl ()
-	  else
-	    p)
+       (fun key (name, depr, (sync,read,_,_,_)) p ->
+	  if sync then p ++ print_option key name (read ()) depr
+	  else p)
        !value_tab (mt ()) ++
      str "Asynchronous options:" ++ fnl () ++
      OptionMap.fold
-       (fun key (name,(sync,read,_,_,_)) p ->
-	  if sync then
-	    p
-	  else
-	    p ++ str ("  "^(nickname key)^": ") ++
-            msg_option_value (name,read()) ++ fnl ())
+       (fun key (name, depr, (sync,read,_,_,_)) p ->
+	  if sync then p
+	  else p ++ print_option key name (read ()) depr)
        !value_tab (mt ()) ++
      str "Tables:" ++ fnl () ++
      List.fold_right
diff --git a/library/goptions.mli b/library/goptions.mli
index 78c4d8e6..d25c1202 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -1,16 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: goptions.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** This module manages customization parameters at the vernacular level     *)
 
-(* This module manages customization parameters at the vernacular level     *)
-
-(* Two kinds of things are managed : tables and options value
+(** Two kinds of things are managed : tables and options value
    - Tables are created by applying the [MakeTable] functor.
    - Variables storing options value are created by applying one of the
    [declare_int_option], [declare_bool_option], ... functions.
@@ -40,12 +38,11 @@
 
        Set Tata Tutu Titi.
        Unset Tata Tutu Titi.
-       Print Table Tata Tutu Titi. (* synonym: Test Table Tata Tutu Titi. *)
+       Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *)
 
    The created table/option may be declared synchronous or not
    (synchronous = consistent with the resetting commands)                   *)
 
-(*i*)
 open Pp
 open Util
 open Names
@@ -53,18 +50,12 @@ open Libnames
 open Term
 open Nametab
 open Mod_subst
-(*i*)
-
-(*s Things common to tables and options. *)
-
-(* The type of table/option keys *)
-type option_name = string list
 
-val error_undeclared_key : option_name -> 'a
+type option_name = Goptionstyp.option_name
 
-(*s Tables. *)
+(** {6 Tables. } *)
 
-(* The functor [MakeStringTable] declares a table containing objects
+(** The functor [MakeStringTable] declares a table containing objects
    of type [string]; the function [member_message] say what to print
    when invoking the "Test Toto Titi foo." command; at the end [title]
    is the table name printed when invoking the "Print Toto Titi."
@@ -85,7 +76,7 @@ sig
   val elements : unit -> string list
 end
 
-(* The functor [MakeRefTable] declares a new table of objects of type
+(** The functor [MakeRefTable] declares a new table of objects of type
    [A.t] practically denoted by [reference]; the encoding function
    [encode : reference -> A.t] is typically a globalization function,
    possibly with some restriction checks; the function
@@ -113,21 +104,26 @@ module MakeRefTable :
     end
 
 
-(*s Options. *)
+(** {6 Options. } *)
 
-(* These types and function are for declaring a new option of name [key]
+(** These types and function are for declaring a new option of name [key]
    and access functions [read] and [write]; the parameter [name] is the option name
    used when printing the option value (command "Print Toto Titi." *)
 
 type 'a option_sig = {
   optsync    : bool;
+  (** whether the option is synchronous w.r.t to the section/module system. *)
+  optdepr    : bool;
+  (** whether the option is DEPRECATED *)
   optname    : string;
+  (** a short string describing the option *)
   optkey     : option_name;
+  (** the low-level name of this option *)
   optread    : unit -> 'a;
   optwrite   : 'a -> unit
 }
 
-(* When an option is declared synchronous ([optsync] is [true]), the output is
+(** When an option is declared synchronous ([optsync] is [true]), the output is
    a synchronous write function. Otherwise it is [optwrite] *)
 
 type 'a write_function = 'a -> unit
@@ -137,7 +133,9 @@ val declare_bool_option  : bool option_sig   -> bool write_function
 val declare_string_option: string option_sig -> string write_function
 
 
-(*s Special functions supposed to be used only in vernacentries.ml *)
+(** {6 Special functions supposed to be used only in vernacentries.ml } *)
+
+module OptionMap : Map.S with type key = option_name
 
 val get_string_table :
   option_name ->
@@ -153,7 +151,8 @@ val get_ref_table :
       mem : reference -> unit;
       print : unit >
 
-(* The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *)
+(** The first argument is a locality flag.
+    [Some true] = "Local", [Some false]="Global". *)
 val set_int_option_value_gen    : bool option -> option_name -> int option -> unit
 val set_bool_option_value_gen   : bool option -> option_name -> bool   -> unit
 val set_string_option_value_gen : bool option -> option_name -> string -> unit
@@ -165,5 +164,7 @@ val set_string_option_value : option_name -> string -> unit
 
 val print_option_value : option_name -> unit
 
+val get_tables : unit -> Goptionstyp.option_state OptionMap.t
 val print_tables : unit -> unit
 
+val error_undeclared_key : option_name -> 'a
diff --git a/library/goptionstyp.mli b/library/goptionstyp.mli
new file mode 100644
index 00000000..541a1470
--- /dev/null
+++ b/library/goptionstyp.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Some types used in the generic option mechanism (Goption) *)
+
+(** Placing them here in a pure interface avoid some dependency issues
+    when compiling CoqIDE *)
+
+type option_name = string list
+
+type option_value =
+  | BoolValue   of bool
+  | IntValue    of int option
+  | StringValue of string
+
+type option_state = {
+  opt_sync  : bool;
+  opt_depr  : bool;
+  opt_name  : string;
+  opt_value : option_value;
+}
diff --git a/library/heads.ml b/library/heads.ml
index 8244761d..9f9f1ca2 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: heads.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
 open Util
 open Names
@@ -150,7 +148,7 @@ let cache_head o =
 let subst_head_approximation subst = function
   | RigidHead (RigidParameter cst) as k ->
       let cst,c = subst_con subst cst in
-      if c = mkConst cst then
+      if isConst c && eq_constant (destConst c) cst then
         (* A change of the prefix of the constant *)
         k
       else
@@ -169,7 +167,9 @@ let discharge_head (_,(ref,k)) =
 let rebuild_head (ref,k) =
   (ref, compute_head ref)
 
-let (inHead, _) =
+type head_obj = evaluable_global_reference * head_approximation
+
+let inHead : head_obj -> obj =
   declare_object {(default_object "HEAD") with
     cache_function = cache_head;
     load_function = load_head;
diff --git a/library/heads.mli b/library/heads.mli
index e13b171f..9e80c173 100644
--- a/library/heads.mli
+++ b/library/heads.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: heads.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Names
 open Term
 open Environ
@@ -17,12 +15,12 @@ open Environ
     provides the function to compute the head symbols and a table to
     store the heads *)
 
-(* [declared_head] computes and registers the head symbol of a
+(** [declared_head] computes and registers the head symbol of a
    possibly evaluable constant or variable *)
 
 val declare_head : evaluable_global_reference -> unit
 
-(* [is_rigid] tells if some term is known to ultimately reduce to a term
+(** [is_rigid] tells if some term is known to ultimately reduce to a term
     with a rigid head symbol *)
 
 val is_rigid : env -> constr -> bool
diff --git a/library/impargs.ml b/library/impargs.ml
index 1c2b5afe..ef7f5921 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Names
 open Libnames
@@ -159,7 +157,7 @@ let is_flexible_reference env bound depth f =
     | Rel n -> (* since local definitions have been expanded *) false
     | Const kn ->
         let cb = Environ.lookup_constant kn env in
-        cb.const_body <> None & not cb.const_opaque
+	(match cb.const_body with Def _ -> true | _ -> false)
     | Var id ->
         let (_,value,_) = Environ.lookup_named id env in value <> None
     | Ind _ | Construct _ -> false
@@ -248,6 +246,10 @@ let compute_auto_implicits env flags enriching t =
   if enriching then compute_implicits_flags env flags true t
   else compute_implicits_gen false false false true true env t
 
+let compute_implicits_names env t =
+  let _, impls = compute_implicits_gen false false false false true env t in
+  List.map fst impls
+
 (* Extra information about implicit arguments *)
 
 type maximal_insertion = bool (* true = maximal contextual insertion *)
@@ -439,9 +441,6 @@ let merge_impls (cond,oldimpls) (_,newimpls) =
     | Some (_, Manual, _) -> orig
     | _ -> ni) oldimpls newimpls)@usersuffiximpls
 
-let merge_impls_list oldimpls newimpls =
-  merge_impls oldimpls newimpls
-
 (* Caching implicits *)
 
 type implicit_interactive_request =
@@ -458,7 +457,18 @@ type implicit_discharge_request =
 let implicits_table = ref Refmap.empty
 
 let implicits_of_global ref =
-  try Refmap.find ref !implicits_table with Not_found -> [DefaultImpArgs,[]]
+  try
+    let l = Refmap.find ref !implicits_table in
+    try
+      let rename_l = Arguments_renaming.arguments_names ref in
+      let rename imp name = match imp, name with
+       | Some (_, x,y), Name id -> Some (id, x,y)
+       | _ -> imp in
+      List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
+    with Not_found -> l
+    | Invalid_argument _ ->
+        anomaly "renamings list and implicits list have different lenghts"
+  with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
   implicits_table := Refmap.add ref imps !implicits_table
@@ -496,18 +506,23 @@ let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
+    (try
       let vars = section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
       let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
       Some (ImplInteractive (ref',flags,exp),l')
+    with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
+    (try
       let con' = pop_con con in
       let vars = section_segment_of_constant con in
       let extra_impls = impls_of_context vars in
       let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
 	Some (ImplConstant (con',flags),l')
+    with Not_found -> (* con not defined in this section *) Some (req,l))
   | ImplMutualInductive (kn,flags) ->
+    (try
       let l' = List.map (fun (gr, l) ->
 	let vars = section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
@@ -515,6 +530,7 @@ let discharge_implicits (_,(req,l)) =
 	 List.map (add_section_impls vars extra_impls) l)) l
       in
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
+    with Not_found -> (* ref not defined in this section *) Some (req,l))
 
 let rebuild_implicits (req,l) =
   match req with
@@ -553,7 +569,11 @@ let rebuild_implicits (req,l) =
 let classify_implicits (req,_ as obj) =
   if req = ImplLocal then Dispose else Substitute obj
 
-let (inImplicits, _) =
+type implicits_obj =
+    implicit_discharge_request *
+      (global_reference * implicits_list list) list
+
+let inImplicits : implicits_obj -> obj =
   declare_object {(default_object "IMPLICITS") with
     cache_function = cache_implicits;
     load_function = load_implicits;
@@ -593,6 +613,8 @@ let declare_mib_implicits kn =
 (* Declare manual implicits *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
+type manual_implicits = manual_explicitation list
+
 let compute_implicits_with_manual env typ enriching l =
   let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in
   set_manual_implicits env !implicit_args enriching autoimpls l
diff --git a/library/impargs.mli b/library/impargs.mli
index 7ec7767b..04251f33 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -1,22 +1,19 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: impargs.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Libnames
 open Term
 open Environ
 open Nametab
-(*i*)
 
-(*s Implicit arguments. Here we store the implicit arguments. Notice that we
+(** {6 Implicit Arguments } *)
+(** Here we store the implicit arguments. Notice that we
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
@@ -36,7 +33,8 @@ val is_maximal_implicit_args : unit -> bool
 type implicits_flags
 val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
 
-(*s An [implicits_list] is a list of positions telling which arguments
+(** {6 ... } *)
+(** An [implicits_list] is a list of positions telling which arguments
     of a reference can be automatically infered *)
 
 
@@ -44,13 +42,35 @@ type argument_position =
   | Conclusion
   | Hyp of int
 
+(** We remember various information about why an argument is
+   inferable as implicit *)
 type implicit_explanation =
   | DepRigid of argument_position
+      (** means that the implicit argument can be found by
+	  unification along a rigid path (we do not print the arguments of
+	  this kind if there is enough arguments to infer them) *)
   | DepFlex of argument_position
+      (** means that the implicit argument can be found by unification
+	  along a collapsable path only (e.g. as x in (P x) where P is another
+	  argument) (we do (defensively) print the arguments of this kind) *)
   | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
+      (** means that the least argument from which the
+	  implicit argument can be inferred is following a collapsable path
+	  but there is a greater argument from where the implicit argument is
+	  inferable following a rigid path (useful to know how to print a
+	  partial application) *)
   | Manual
+      (** means the argument has been explicitely set as implicit. *)
+      
+(**  We also consider arguments inferable from the conclusion but it is
+     operational only if [conclusion_matters] is true. *)
+
+type maximal_insertion = bool (** true = maximal contextual insertion *)
+type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
 
-type implicit_status = (identifier * implicit_explanation * (bool * bool)) option
+type implicit_status = (identifier * implicit_explanation * 
+			  (maximal_insertion * force_inference)) option
+    (** [None] = Not implicit *)
 
 type implicit_side_condition
 
@@ -64,19 +84,20 @@ val force_inference_of : implicit_status -> bool
 
 val positions_of_implicits : implicits_list -> int list
 
-(* Computation of the positions of arguments automatically inferable
-   for an object of the given type in the given env *)
-val compute_implicits : env -> types -> implicits_list list
-
-(* A [manual_explicitation] is a tuple of a positional or named explicitation with
+(** A [manual_explicitation] is a tuple of a positional or named explicitation with
    maximal insertion, force inference and force usage flags. Forcing usage makes
    the argument implicit even if the automatic inference considers it not inferable. *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
+type manual_explicitation = Topconstr.explicitation * 
+    (maximal_insertion * force_inference * bool)
+
+type manual_implicits = manual_explicitation list
 
 val compute_implicits_with_manual : env -> types -> bool ->
-  manual_explicitation list -> implicit_status list
+  manual_implicits -> implicit_status list
+
+val compute_implicits_names : env -> types -> name list
 
-(*s Computation of implicits (done using the global environment). *)
+(** {6 Computation of implicits (done using the global environment). } *)
 
 val declare_var_implicits : variable -> unit
 val declare_constant_implicits : constant -> unit
@@ -84,28 +105,26 @@ val declare_mib_implicits : mutual_inductive -> unit
 
 val declare_implicits : bool -> global_reference -> unit
 
-(* [declare_manual_implicits local ref enriching l]
+(** [declare_manual_implicits local ref enriching l]
    Manual declaration of which arguments are expected implicit.
    If not set, we decide if it should enrich by automatically inferd
    implicits depending on the current state.
    Unsets implicits if [l] is empty. *)
 
 val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
-  manual_explicitation list list -> unit
+  manual_implicits list -> unit
 
-(* If the list is empty, do nothing, otherwise declare the implicits. *)
+(** If the list is empty, do nothing, otherwise declare the implicits. *)
 
 val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
-  manual_explicitation list -> unit
+  manual_implicits -> unit
 
 val implicits_of_global : global_reference -> implicits_list list
 
 val extract_impargs_data :
   implicits_list list -> ((int * int) option * implicit_status list) list
 
-val lift_implicits : int -> manual_explicitation list -> manual_explicitation list
-
-val merge_impls : implicits_list -> implicits_list -> implicits_list
+val lift_implicits : int -> manual_implicits -> manual_implicits
 
 val make_implicits_list : implicit_status list -> implicits_list list
 
@@ -115,9 +134,7 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list
 
 val select_stronger_impargs : implicits_list list -> implicit_status list
 
-type implicit_interactive_request =
-  | ImplAuto
-  | ImplManual of int
+type implicit_interactive_request
 
 type implicit_discharge_request =
   | ImplLocal
diff --git a/library/lib.ml b/library/lib.ml
index 6f8655d3..7554fd0b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -1,26 +1,26 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
 open Util
 open Libnames
 open Nameops
 open Libobject
 open Summary
+
+type is_type = bool (* Module Type or just Module *)
+type export = bool option (* None for a Module Type *)
+
 type node =
   | Leaf of obj
   | CompilingLibrary of object_prefix
-  | OpenedModule of bool option * object_prefix * Summary.frozen
+  | OpenedModule of is_type * export * object_prefix * Summary.frozen
   | ClosedModule  of library_segment
-  | OpenedModtype of object_prefix * Summary.frozen
-  | ClosedModtype of library_segment
   | OpenedSection of object_prefix * Summary.frozen
   | ClosedSection of library_segment
   | FrozenState of Summary.frozen
@@ -31,6 +31,9 @@ and library_segment = library_entry list
 
 type lib_objects =  (Names.identifier * obj) list
 
+let module_kind is_type =
+  if is_type then "module type" else "module"
+
 let iter_objects f i prefix =
   List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
 
@@ -69,10 +72,9 @@ let classify_segment seg =
     (* LEM; TODO: Understand what this does and see if what I do is the
                   correct thing for ClosedMod(ule|type) *)
     | (_,ClosedModule _) :: stk -> clean acc stk
-    | (_,ClosedModtype _) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
-    | (_,OpenedModule _) :: _ -> error "there are still opened modules"
-    | (_,OpenedModtype _) :: _ -> error "there are still opened module types"
+    | (_,OpenedModule (ty,_,_,_)) :: _ ->
+      error ("there are still opened " ^ module_kind ty ^"s")
     | (_,FrozenState _) :: stk -> clean acc stk
   in
     clean ([],[],[]) (List.rev seg)
@@ -144,8 +146,7 @@ let make_oname id = make_path id, make_kn id
 let recalc_path_prefix () =
   let rec recalc = function
     | (sp, OpenedSection (dir,_)) :: _ -> dir
-    | (sp, OpenedModule (_,dir,_)) :: _ -> dir
-    | (sp, OpenedModtype (dir,_)) :: _ -> dir
+    | (sp, OpenedModule (_,_,dir,_)) :: _ -> dir
     | (sp, CompilingLibrary dir) :: _ -> dir
     | _::l -> recalc l
     | [] -> initial_prefix
@@ -181,7 +182,6 @@ let split_lib_gen test =
 	then Some (collect after [hd] before)
 	else (match hd with
 		| (sp,ClosedModule  seg)
-		| (sp,ClosedModtype seg)
 		| (sp,ClosedSection seg) ->
 		    (match findeq after seg with
 		       | None -> findeq (hd::after) before
@@ -197,11 +197,11 @@ let split_lib_gen test =
 let split_lib sp = split_lib_gen (fun x -> fst x = sp)
 
 let split_lib_at_opening sp =
-  let a,s,b = split_lib_gen (function
-    | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) ->
-	x = sp
-    | _ ->
-	false) in
+  let is_sp = function
+    | x,(OpenedSection _|OpenedModule _|CompilingLibrary _) -> x = sp
+    | _ -> false
+  in
+  let a,s,b = split_lib_gen is_sp in
   assert (List.tl s = []);
   (a,List.hd s,b)
 
@@ -254,97 +254,66 @@ let add_frozen_state () =
 
 (* Modules. *)
 
-
-let is_opened id = function
-    oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when
-      basename (fst oname) = id -> true
-  | _ -> false
-
 let is_opening_node = function
-    _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true
+  | _,(OpenedSection _ | OpenedModule _) -> true
   | _ -> false
 
+let is_opening_node_or_lib = function
+  | _,(CompilingLibrary _ | OpenedSection _ | OpenedModule _) -> true
+  | _ -> false
 
 let current_mod_id () =
-  try match find_entry_p is_opening_node with
-    | oname,OpenedModule (_,_,fs) ->
-	basename (fst oname)
-    | oname,OpenedModtype (_,fs) ->
-	basename (fst oname)
+  try match find_entry_p is_opening_node_or_lib with
+    | oname,OpenedModule (_,_,_,fs) -> basename (fst oname)
+    | oname,CompilingLibrary _ -> basename (fst oname)
     | _ -> error "you are not in a module"
-  with Not_found ->
-    error "no opened modules"
+  with Not_found -> error "no opened modules"
 
 
-let start_module export id mp fs =
+let start_mod is_type export id mp fs =
   let dir = add_dirpath_suffix (fst !path_prefix) id in
   let prefix = dir,(mp,Names.empty_dirpath) in
-  let oname = make_path id, make_kn id in
-  if Nametab.exists_module dir then
-    errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
-  add_entry oname (OpenedModule (export,prefix,fs));
+  let sp = make_path id in
+  let oname = sp, make_kn id in
+  let exists =
+    if is_type then Nametab.exists_cci sp else Nametab.exists_module dir
+  in
+  if exists then
+    errorlabstrm "open_module" (pr_id id ++ str " already exists");
+  add_entry oname (OpenedModule (is_type,export,prefix,fs));
   path_prefix := prefix;
   prefix
 (*  add_frozen_state () must be called in declaremods *)
 
+let start_module = start_mod false
+let start_modtype = start_mod true None
+
 let error_still_opened string oname =
   let id = basename (fst oname) in
-  errorlabstrm "" (str string ++ spc () ++ pr_id id ++ str " is still opened.")
+  errorlabstrm ""
+    (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.")
 
-let end_module () =
+let end_mod is_type =
   let oname,fs =
     try match find_entry_p is_opening_node with
-      | oname,OpenedModule (_,_,fs) -> oname,fs
-      | oname,OpenedModtype _ -> error_still_opened "Module Type" oname
-      | oname,OpenedSection _ -> error_still_opened "Section" oname
+      | oname,OpenedModule (ty,_,_,fs) ->
+	if ty = is_type then oname,fs
+	else error_still_opened (module_kind ty) oname
+      | oname,OpenedSection _ -> error_still_opened "section" oname
       | _ -> assert false
-    with Not_found ->
-      error "No opened modules."
+    with Not_found -> error "No opened modules."
   in
   let (after,mark,before) = split_lib_at_opening oname in
   lib_stk := before;
   add_entry oname (ClosedModule (List.rev (mark::after)));
   let prefix = !path_prefix in
-  (* LEM: This module business seems more complicated than sections;
-          shouldn't a backtrack into a closed module also do something
-          with global.ml, given that closing a module does?
-     TODO
-   *)
   recalc_path_prefix ();
   (* add_frozen_state must be called after processing the module,
      because we cannot recache interactive modules  *)
   (oname, prefix, fs, after)
 
-let start_modtype id mp fs =
-  let dir = add_dirpath_suffix (fst !path_prefix) id in
-  let prefix = dir,(mp,Names.empty_dirpath) in
-  let sp = make_path id in
-  let name = sp, make_kn id in
-  if Nametab.exists_cci sp then
-    errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ;
-  add_entry name (OpenedModtype (prefix,fs));
-  path_prefix := prefix;
-  prefix
-
-let end_modtype () =
-  let oname,fs =
-    try match find_entry_p is_opening_node with
-      | oname,OpenedModtype (_,fs) -> oname,fs
-      | oname,OpenedModule _ -> error_still_opened "Module" oname
-      | oname,OpenedSection _ -> error_still_opened "Section" oname
-      | _ -> assert false
-    with Not_found ->
-      error "no opened module types"
-  in
-  let (after,mark,before) = split_lib_at_opening oname in
-  lib_stk := before;
-  add_entry oname (ClosedModtype (List.rev (mark::after)));
-  let dir = !path_prefix in
-  recalc_path_prefix ();
-  (* add_frozen_state must be called after processing the module type.
-     This is because we cannot recache interactive module types *)
-  (oname,dir,fs,after)
-
+let end_module () = end_mod false
+let end_modtype () = end_mod true
 
 let contents_after = function
   | None -> !lib_stk
@@ -352,13 +321,6 @@ let contents_after = function
 
 (* Modules. *)
 
-let check_for_comp_unit () =
-  let is_decl = function (_,FrozenState _) -> false | _ -> true in
-  try
-    let _ = find_entry_p is_decl in
-    error "a module cannot be started after some declarations"
-  with Not_found -> ()
-
 (* TODO: use check_for_module ? *)
 let start_compilation s mp =
   if !comp_name <> None then
@@ -374,21 +336,18 @@ let end_compilation dir =
   let _ =
     try match snd (find_entry_p is_opening_node) with
       | OpenedSection _ -> error "There are some open sections."
-      | OpenedModule _ -> error "There are some open modules."
-      | OpenedModtype _ -> error "There are some open module types."
+      | OpenedModule (ty,_,_,_) ->
+	error ("There are some open "^module_kind ty^"s.")
       | _ -> assert false
-    with
-	Not_found -> ()
+    with Not_found -> ()
   in
-  let module_p =
-    function (_,CompilingLibrary _) -> true | x -> is_opening_node x
+  let is_opening_lib = function _,CompilingLibrary _ -> true | _ -> false
   in
   let oname =
-    try match find_entry_p module_p with
-	(oname, CompilingLibrary prefix) -> oname
+    try match find_entry_p is_opening_lib with
+      |	(oname, CompilingLibrary prefix) -> oname
       | _ -> assert false
-    with
-	Not_found -> anomaly "No module declared"
+    with Not_found -> anomaly "No module declared"
   in
   let _ =
     match !comp_name with
@@ -399,31 +358,23 @@ let end_compilation dir =
 	       " and not " ^ (Names.string_of_dirpath m));
   in
   let (after,mark,before) = split_lib_at_opening oname in
-    comp_name := None;
-    !path_prefix,after
+  comp_name := None;
+  !path_prefix,after
 
-(* Returns true if we are inside an opened module type *)
-let is_modtype () =
-  let opened_p = function
-    | _, OpenedModtype _ -> true
-    | _ -> false
-  in
-    try
-      let _ = find_entry_p opened_p in true
-    with
-	Not_found -> false
-
-(* Returns true if we are inside an opened module *)
-let is_module () =
-  let opened_p = function
-    | _, OpenedModule _ -> true
+(* Returns true if we are inside an opened module or module type *)
+
+let is_module_gen which =
+  let test = function
+    | _, OpenedModule (ty,_,_,_) -> which ty
     | _ -> false
   in
-    try
-      let _ = find_entry_p opened_p in true
-    with
-	Not_found -> false
+  try
+    let _ = find_entry_p test in true
+  with Not_found -> false
 
+let is_module_or_modtype () = is_module_gen (fun _ -> true)
+let is_modtype () = is_module_gen (fun b -> b)
+let is_module () = is_module_gen (fun b -> not b)
 
 (* Returns the opening node of a given name *)
 let find_opening_node id =
@@ -495,8 +446,6 @@ let add_section_constant kn =
 
 let replacement_context () = pi2 (List.hd !sectab)
 
-let variables_context () = pi1 (List.hd !sectab)
-
 let section_segment_of_constant con =
   Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
 
@@ -563,8 +512,8 @@ let discharge_item ((sp,_ as oname),e) =
   | Leaf lobj ->
       Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
   | FrozenState _ -> None
-  | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None
-  | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ ->
+  | ClosedSection _ | ClosedModule _ -> None
+  | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly "discharge_item"
 
 let close_section () =
@@ -590,8 +539,8 @@ let close_section () =
 (*****************)
 (* Backtracking. *)
 
-let (inLabel,outLabel) =
-  declare_object {(default_object "DOT") with
+let (inLabel : int -> obj), (outLabel : obj -> int) =
+  declare_object_full {(default_object "DOT") with
 				classify_function = (fun _ -> Dispose)}
 
 let recache_decl = function
@@ -604,13 +553,6 @@ let recache_context ctx =
 
 let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
 
-let has_top_frozen_state () =
-  let rec aux = function
-  | (sp, FrozenState _)::_ -> Some sp
-  | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t
-  | _ -> None
-  in aux !lib_stk
-
 let set_lib_stk new_lib_stk =
   lib_stk := new_lib_stk;
   recalc_path_prefix ();
@@ -630,17 +572,9 @@ let reset_to_gen test =
 
 let reset_to sp = reset_to_gen (fun x -> fst x = sp)
 
-let reset_to_state sp =
-  let (_,eq,before) = split_lib sp in
-  (* if eq a frozen state, we'll reset to it *)
-  match eq with
-  | [_,FrozenState f] -> lib_stk := eq@before; recalc_path_prefix (); unfreeze_summaries f
-  | _ -> error "Not a frozen state"
-
-
 (* LEM: TODO
  * We will need to muck with frozen states in after, too!
- * Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype)
+ * Not only FrozenState, but also those embedded in Opened(Section|Module)
  *)
 let delete_gen test =
   let (after,equal,before) = split_lib_gen test in
@@ -676,8 +610,8 @@ let remove_name (loc,id) =
     delete sp
 
 let is_mod_node = function
-  | OpenedModule _ | OpenedModtype _ | OpenedSection _
-  | ClosedModule _ | ClosedModtype _ | ClosedSection _  -> true
+  | OpenedModule _ | OpenedSection _
+  | ClosedModule _ | ClosedSection _  -> true
   | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
 	|| t = "MODULE ALIAS"
   | _ -> false
@@ -710,17 +644,16 @@ let is_label_n n x =
     | (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true
     | _ -> false
 
-(* Reset the label registered by [mark_end_of_command()] with number n. *)
+(** Reset the label registered by [mark_end_of_command()] with number n,
+    which should be strictly in the past. *)
+
 let reset_label n =
-  let current = current_command_label() in
-  if n < current then
-    let res = reset_to_gen (is_label_n n) in
-    set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
-    res
-  else (* optimisation to avoid recaching when not necessary (why is it so long??) *)
-    match !lib_stk with
-      | [] -> ()
-      | x :: ls -> (lib_stk := ls;set_command_label (n-1))
+  if n >= current_command_label () then
+    error "Cannot backtrack to the current label or a future one";
+  let res = reset_to_gen (is_label_n n) in
+  (* forget state numbers after n only if reset succeeded *)
+  set_command_label (n-1);
+  res
 
 let rec back_stk n stk =
   match stk with
@@ -729,7 +662,9 @@ let rec back_stk n stk =
     | _::tail -> back_stk n tail
     | [] -> error "Reached begin of command history"
 
-let back n = reset_to (back_stk n !lib_stk)
+let back n =
+  reset_to (back_stk n !lib_stk);
+  set_command_label (current_command_label () - n - 1)
 
 (* State and initialization. *)
 
@@ -793,7 +728,7 @@ let rec split_mp mp =
     | Names.MPdot (prfx, lbl) ->
 	let mprec, dprec = split_mp prfx in
 	  mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
-    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
+    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [id]
 
 let split_modpath mp =
   let rec aux = function
diff --git a/library/lib.mli b/library/lib.mli
index 7eb8b688..0d6eb34b 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -1,25 +1,26 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lib.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
+(** Lib: record of operations, backtrack, low-level sections *)
 
-(*s This module provides a general mechanism to keep a trace of all operations
+(** This module provides a general mechanism to keep a trace of all operations
    and to backtrack (undo) those operations. It provides also the section
    mechanism (at a low level; discharge is not known at this step). *)
 
+type is_type = bool (* Module Type or just Module *)
+type export = bool option (* None for a Module Type *)
+
 type node =
   | Leaf of Libobject.obj
   | CompilingLibrary of Libnames.object_prefix
-  | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen
+  | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen
   | ClosedModule  of library_segment
-  | OpenedModtype of Libnames.object_prefix * Summary.frozen
-  | ClosedModtype of library_segment
   | OpenedSection of Libnames.object_prefix * Summary.frozen
   | ClosedSection of library_segment
   | FrozenState of Summary.frozen
@@ -28,14 +29,14 @@ and library_segment = (Libnames.object_name * node) list
 
 type lib_objects = (Names.identifier * Libobject.obj) list
 
-(*s Object iteratation functions. *)
+(** {6 Object iteration functions. } *)
 
 val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
 val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
 val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects
 (*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
 
-(* [classify_segment seg] verifies that there are no OpenedThings,
+(** [classify_segment seg] verifies that there are no OpenedThings,
    clears ClosedSections and FrozenStates and divides Leafs according
    to their answers to the [classify_object] function in three groups:
    [Substitute], [Keep], [Anticipate] respectively.  The order of each
@@ -43,41 +44,45 @@ val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects
 val classify_segment :
   library_segment -> lib_objects * lib_objects * Libobject.obj list
 
-(* [segment_of_objects prefix objs] forms a list of Leafs *)
+(** [segment_of_objects prefix objs] forms a list of Leafs *)
 val segment_of_objects :
   Libnames.object_prefix -> lib_objects -> library_segment
 
 
-(*s Adding operations (which call the [cache] method, and getting the
+(** {6 ... } *)
+(** Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
 val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name
 val add_anonymous_leaf : Libobject.obj -> unit
 
-(* this operation adds all objects with the same name and calls [load_object]
+(** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
 val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
 
 val add_frozen_state : unit -> unit
 
-(* Adds a "dummy" entry in lib_stk with a unique new label number. *)
+(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
 val mark_end_of_command : unit -> unit
-(* Returns the current label number *)
+
+(** Returns the current label number *)
 val current_command_label : unit -> int
-(* [reset_label n ] resets [lib_stk] to the label n registered by
-   [mark_end_of_command()]. That is it forgets the label and anything
-   registered after it. *)
+
+(** [reset_label n] resets [lib_stk] to the label n registered by
+   [mark_end_of_command()]. It forgets the label and anything
+   registered after it. The label should be strictly in the past. *)
 val reset_label : int -> unit
 
-(*s The function [contents_after] returns the current library segment,
+(** {6 ... } *)
+(** The function [contents_after] returns the current library segment,
   starting from a given section path. If not given, the entire segment
   is returned. *)
 
 val contents_after : Libnames.object_name option -> library_segment
 
-(*s Functions relative to current path *)
+(** {6 Functions relative to current path } *)
 
-(* User-side names *)
+(** User-side names *)
 val cwd : unit -> Names.dir_path
 val cwd_except_section : unit -> Names.dir_path
 val current_dirpath : bool -> Names.dir_path (* false = except sections *)
@@ -85,72 +90,79 @@ val make_path : Names.identifier -> Libnames.full_path
 val make_path_except_section : Names.identifier -> Libnames.full_path
 val path_of_include : unit -> Libnames.full_path
 
-(* Kernel-side names *)
+(** Kernel-side names *)
 val current_prefix : unit -> Names.module_path * Names.dir_path
 val make_kn : Names.identifier -> Names.kernel_name
 val make_con : Names.identifier -> Names.constant
 
-(* Are we inside an opened section *)
+(** Are we inside an opened section *)
 val sections_are_opened : unit -> bool
 val sections_depth : unit -> int
 
-(* Are we inside an opened module type *)
+(** Are we inside an opened module type *)
+val is_module_or_modtype : unit -> bool
 val is_modtype : unit -> bool
 val is_module : unit -> bool
 val current_mod_id : unit -> Names.module_ident
 
-(* Returns the opening node of a given name *)
+(** Returns the opening node of a given name *)
 val find_opening_node : Names.identifier -> node
 
-(*s Modules and module types *)
+(** {6 Modules and module types } *)
 
 val start_module :
-  bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
-val end_module : unit
-  -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
+  export -> Names.module_ident -> Names.module_path ->
+  Summary.frozen -> Libnames.object_prefix
 
 val start_modtype :
-  Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
-val end_modtype : unit
-  -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
-(* [Lib.add_frozen_state] must be called after each of the above functions *)
+  Names.module_ident -> Names.module_path ->
+  Summary.frozen -> Libnames.object_prefix
+
+val end_module :
+  unit ->
+  Libnames.object_name * Libnames.object_prefix *
+    Summary.frozen * library_segment
 
-(*s Compilation units *)
+val end_modtype :
+  unit ->
+  Libnames.object_name * Libnames.object_prefix *
+    Summary.frozen * library_segment
+
+(** [Lib.add_frozen_state] must be called after each of the above functions *)
+
+(** {6 Compilation units } *)
 
 val start_compilation : Names.dir_path -> Names.module_path -> unit
 val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment
 
-(* The function [library_dp] returns the [dir_path] of the current
+(** The function [library_dp] returns the [dir_path] of the current
    compiling library (or [default_library]) *)
 val library_dp : unit -> Names.dir_path
 
-(* Extract the library part of a name even if in a section *)
+(** Extract the library part of a name even if in a section *)
 val dp_of_mp : Names.module_path -> Names.dir_path
 val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
 val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list
 val library_part :  Libnames.global_reference -> Names.dir_path
 val remove_section_part : Libnames.global_reference -> Names.dir_path
 
-(*s Sections *)
+(** {6 Sections } *)
 
 val open_section : Names.identifier -> unit
 val close_section : unit -> unit
 
-(*s Backtracking (undo). *)
+(** {6 Backtracking (undo). } *)
 
 val reset_to : Libnames.object_name -> unit
 val reset_name : Names.identifier Util.located -> unit
 val remove_name : Names.identifier Util.located -> unit
 val reset_mod : Names.identifier Util.located -> unit
-val reset_to_state : Libnames.object_name -> unit
-
-val has_top_frozen_state : unit -> Libnames.object_name option
 
-(* [back n] resets to the place corresponding to the $n$-th call of
+(** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of
    [mark_end_of_command] (counting backwards) *)
 val back : int -> unit
 
-(*s We can get and set the state of the operations (used in [States]). *)
+(** {6 We can get and set the state of the operations (used in [States]). } *)
 
 type frozen
 
@@ -163,13 +175,13 @@ val declare_initial_state : unit -> unit
 val reset_initial : unit -> unit
 
 
-(* XML output hooks *)
+(** XML output hooks *)
 val set_xml_open_section : (Names.identifier -> unit) -> unit
 val set_xml_close_section : (Names.identifier -> unit) -> unit
 
 type binding_kind = Explicit | Implicit
 
-(*s Section management for discharge *)
+(** {6 Section management for discharge } *)
 type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types
 type variable_context = variable_info list
 
@@ -189,7 +201,7 @@ val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit
 val replacement_context : unit ->
   (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t)
 
-(*s Discharge: decrease the section level if in the current section *)
+(** {6 Discharge: decrease the section level if in the current section } *)
 
 val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
diff --git a/library/libnames.ml b/library/libnames.ml
index 2986940d..b91d24bd 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Pp
 open Util
 open Names
@@ -29,8 +27,7 @@ let isConstructRef = function ConstructRef _ -> true | _ -> false
 
 let eq_gr gr1 gr2 =
   match gr1,gr2 with 
-      ConstRef con1, ConstRef con2 ->
-	eq_constant con1 con2
+    | ConstRef con1, ConstRef con2 -> eq_constant con1 con2
     | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2
     | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2
     | _,_ -> gr1=gr2
@@ -58,13 +55,10 @@ let subst_global subst ref = match ref with
 	if c'==c then ref,t else ConstructRef c', t
 
 let canonical_gr = function
-  | ConstRef con -> 
-      ConstRef(constant_of_kn(canonical_con con))
-  | IndRef (kn,i) ->
-      IndRef(mind_of_kn(canonical_mind kn),i)
-  | ConstructRef ((kn,i),j )->
-	  ConstructRef((mind_of_kn(canonical_mind kn),i),j)
-  | VarRef id ->  VarRef id
+  | ConstRef con -> ConstRef(constant_of_kn(canonical_con con))
+  | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i)
+  | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+  | VarRef id -> VarRef id
 
 let global_of_constr c = match kind_of_term c with
   | Const sp -> ConstRef sp
@@ -82,25 +76,37 @@ let constr_of_global = function
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
-(* outside of the kernel, names are ordered on their canonical part *)
+let global_ord_gen fc fmi x y =
+  let ind_ord (indx,ix) (indy,iy) =
+    let c = Pervasives.compare ix iy in
+    if c = 0 then kn_ord (fmi indx) (fmi indy) else c
+  in
+  match x, y with
+    | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
+    | IndRef indx, IndRef indy -> ind_ord indx indy
+    | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
+      let c = Pervasives.compare jx jy in
+      if c = 0 then ind_ord indx indy else c
+    | _, _ -> Pervasives.compare x y
+
+let global_ord_can = global_ord_gen canonical_con canonical_mind
+let global_ord_user = global_ord_gen user_con user_mind
+
+(* By default, [global_reference] are ordered on their canonical part *)
+
 module RefOrdered = struct
   type t = global_reference
-  let compare x y = 
-    let make_name = function
-      | ConstRef con -> 
-	  ConstRef(constant_of_kn(canonical_con con))
-      | IndRef (kn,i) ->
-	  IndRef(mind_of_kn(canonical_mind kn),i)
-      | ConstructRef ((kn,i),j )->
-	  ConstructRef((mind_of_kn(canonical_mind kn),i),j)
-      | VarRef id ->  VarRef id
-    in
-	Pervasives.compare (make_name x) (make_name y)
+  let compare = global_ord_can
+end
+
+module RefOrdered_env = struct
+  type t = global_reference
+  let compare = global_ord_user
 end
-  
+
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
-  
+
 (* Extended global references *)
 
 type syndef_name = kernel_name
@@ -109,6 +115,18 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SynDef of syndef_name
 
+(* We order [extended_global_reference] via their user part
+   (cf. pretty printer) *)
+
+module ExtRefOrdered = struct
+  type t = extended_global_reference
+  let compare x y =
+    match x, y with
+      | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
+      | SynDef knx, SynDef kny -> kn_ord knx kny
+      | _, _ -> Pervasives.compare x y
+end
+
 (**********************************************)
 
 let pr_dirpath sl = (str (string_of_dirpath sl))
@@ -177,6 +195,7 @@ type full_path = {
   basename : identifier }
 
 let make_path pa id = { dirpath = pa; basename = id }
+
 let repr_path { dirpath = pa; basename = id } = (pa,id)
 
 (* parsing and printing of section paths *)
@@ -197,8 +216,6 @@ module SpOrdered =
     let compare = sp_ord
   end
 
-module Spset = Set.Make(SpOrdered)
-module Sppred = Predicate.Make(SpOrdered)
 module Spmap = Map.Make(SpOrdered)
 
 let dirpath sp = let (p,_) = repr_path sp in p
diff --git a/library/libnames.mli b/library/libnames.mli
index a7bc3b52..18b6ac49 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -1,22 +1,18 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Pp
 open Util
 open Names
 open Term
 open Mod_subst
-(*i*)
 
-(*s Global reference is a kernel side type for all references together *)
+(** {6 Global reference is a kernel side type for all references together } *)
 type global_reference =
   | VarRef of variable
   | ConstRef of constant
@@ -40,14 +36,14 @@ val destConstructRef : global_reference -> constructor
 val subst_constructor : substitution -> constructor -> constructor * constr
 val subst_global : substitution -> global_reference -> global_reference * constr
 
-(* Turn a global reference into a construction *)
+(** Turn a global reference into a construction *)
 val constr_of_global : global_reference -> constr
 
-(* Turn a construction denoting a global reference into a global reference;
+(** Turn a construction denoting a global reference into a global reference;
    raise [Not_found] if not a global reference *)
 val global_of_constr : constr -> global_reference
 
-(* Obsolete synonyms for constr_of_global and global_of_constr *)
+(** Obsolete synonyms for constr_of_global and global_of_constr *)
 val constr_of_reference : global_reference -> constr
 val reference_of_constr : constr -> global_reference
 
@@ -55,12 +51,16 @@ module RefOrdered : sig
   type t = global_reference
   val compare : global_reference -> global_reference -> int
 end
-  
+
+module RefOrdered_env : sig
+  type t = global_reference
+  val compare : global_reference -> global_reference -> int
+end
 
 module Refset : Set.S with type elt = global_reference
 module Refmap : Map.S with type key = global_reference
 
-(*s Extended global references *)
+(** {6 Extended global references } *)
 
 type syndef_name = kernel_name
 
@@ -68,19 +68,24 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SynDef of syndef_name
 
-(*s Dirpaths *)
+module ExtRefOrdered : sig
+  type t = extended_global_reference
+  val compare : t -> t -> int
+end
+
+(** {6 Dirpaths } *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
 val dirpath_of_string : string -> dir_path
 val string_of_dirpath : dir_path -> string
 
-(* Pop the suffix of a [dir_path] *)
+(** Pop the suffix of a [dir_path] *)
 val pop_dirpath : dir_path -> dir_path
 
-(* Pop the suffix n times *)
+(** Pop the suffix n times *)
 val pop_dirpath_n : int -> dir_path -> dir_path
 
-(* Give the immediate prefix and basename of a [dir_path] *)
+(** Give the immediate prefix and basename of a [dir_path] *)
 val split_dirpath : dir_path -> dir_path * identifier
 
 val add_dirpath_suffix : dir_path -> module_ident -> dir_path
@@ -95,28 +100,27 @@ val is_dirpath_prefix_of : dir_path -> dir_path -> bool
 module Dirset : Set.S with type elt = dir_path
 module Dirmap : Map.S with type key = dir_path
 
-(*s Full paths are {\em absolute} paths of declarations *)
+(** {6 Full paths are {e absolute} paths of declarations } *)
 type full_path
 
-(* Constructors of [full_path] *)
+(** Constructors of [full_path] *)
 val make_path : dir_path -> identifier -> full_path
 
-(* Destructors of [full_path] *)
+(** Destructors of [full_path] *)
 val repr_path : full_path -> dir_path * identifier
 val dirpath : full_path -> dir_path
 val basename : full_path -> identifier
 
-(* Parsing and printing of section path as ["coq_root.module.id"] *)
+(** Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> full_path
 val string_of_path : full_path -> string
 val pr_path : full_path -> std_ppcmds
 
-module Sppred : Predicate.S with type elt = full_path
 module Spmap  : Map.S with type key = full_path
 
 val restrict_path : int -> full_path -> full_path
 
-(*s Temporary function to brutally form kernel names from section paths *)
+(** {6 Temporary function to brutally form kernel names from section paths } *)
 
 val encode_mind : dir_path -> identifier -> mutual_inductive
 val decode_mind : mutual_inductive -> dir_path * identifier
@@ -124,7 +128,8 @@ val encode_con : dir_path -> identifier -> constant
 val decode_con : constant -> dir_path * identifier
 
 
-(*s A [qualid] is a partially qualified ident; it includes fully
+(** {6 ... } *)
+(** A [qualid] is a partially qualified ident; it includes fully
     qualified names (= absolute names) and all intermediate partial
     qualifications of absolute names, including single identifiers.
     The [qualid] are used to access the name table. *)
@@ -138,14 +143,14 @@ val pr_qualid : qualid -> std_ppcmds
 val string_of_qualid : qualid -> string
 val qualid_of_string : string -> qualid
 
-(* Turns an absolute name, a dirpath, or an identifier into a
+(** Turns an absolute name, a dirpath, or an identifier into a
    qualified name denoting the same name *)
 
 val qualid_of_path : full_path -> qualid
 val qualid_of_dirpath : dir_path -> qualid
 val qualid_of_ident : identifier -> qualid
 
-(* Both names are passed to objects: a "semantic" [kernel_name], which
+(** Both names are passed to objects: a "semantic" [kernel_name], which
    can be substituted and a "syntactic" [full_path] which can be printed
 *)
 
@@ -155,16 +160,17 @@ type object_prefix = dir_path * (module_path * dir_path)
 
 val make_oname : object_prefix -> identifier -> object_name
 
-(* to this type are mapped [dir_path]'s in the nametab *)
+(** to this type are mapped [dir_path]'s in the nametab *)
 type global_dir_reference =
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
   | DirClosedSection of dir_path
-      (* this won't last long I hope! *)
+      (** this won't last long I hope! *)
 
-(*s A [reference] is the user-level notion of name. It denotes either a
+(** {6 ... } *)
+(** A [reference] is the user-level notion of name. It denotes either a
     global name (referred either by a qualified name or by a single
     name) or a variable *)
 
@@ -177,13 +183,13 @@ val string_of_reference : reference -> string
 val pr_reference : reference -> std_ppcmds
 val loc_of_reference : reference -> loc
 
-(*s Popping one level of section in global names *)
+(** {6 Popping one level of section in global names } *)
 
 val pop_con : constant -> constant
 val pop_kn : mutual_inductive-> mutual_inductive
 val pop_global_reference : global_reference -> global_reference
 
-(* Deprecated synonyms *)
+(** Deprecated synonyms *)
 
-val make_short_qualid : identifier -> qualid (* = qualid_of_ident *)
-val qualid_of_sp : full_path -> qualid (* = qualid_of_path *)
+val make_short_qualid : identifier -> qualid (** = qualid_of_ident *)
+val qualid_of_sp : full_path -> qualid (** = qualid_of_path *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 7b61a386..bc62913d 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: libobject.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Names
 open Libnames
@@ -18,7 +16,7 @@ open Mod_subst
    wants to work with restricted Coq programs that have only parts of
    the full capabilities, but may still be able to work correctly for
    limited purposes.  One example is for the graphical interface, that uses
-   such a limite coq process to do only parsing.  It loads .vo files, but
+   such a limited Coq process to do only parsing.  It loads .vo files, but
    is only interested in loading the grammar rule definitions. *)
 
 let relax_flag = ref false;;
@@ -57,7 +55,7 @@ let default_object s = {
    declare_object { (default_object "MY OBJECT") with
        cache_function = fun (sp,a) -> Mytbl.add sp a}
 
-   and the listed functions are only those which definitions accually
+   and the listed functions are only those which definitions actually
    differ from the default.
 
    This helps introducing new functions in objects.
@@ -81,7 +79,7 @@ let object_tag lobj = Dyn.tag lobj
 let cache_tab =
   (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
 
-let declare_object odecl =
+let declare_object_full odecl =
   let na = odecl.object_name in
   let (infun,outfun) = Dyn.create na in
   let cacher (oname,lobj) =
@@ -124,6 +122,8 @@ let declare_object odecl =
 			     dyn_rebuild_function = rebuild };
   (infun,outfun)
 
+let declare_object odecl = fst (declare_object_full odecl)
+
 let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
 
 (* this function describes how the cache, load, open, and export functions
@@ -143,8 +143,9 @@ let apply_dyn_fun deflt f lobj =
     Failure "local to_apply_dyn_fun" ->
       if not (!relax_flag || Hashtbl.mem missing_tab tag) then
         begin
-          Pp.warning ("Cannot find library functions for an object with tag "
-                      ^ tag ^ " (a plugin may be missing)");
+          Pp.msg_warning
+	    (Pp.str ("Cannot find library functions for an object with tag "
+                      ^ tag ^ " (a plugin may be missing)"));
           Hashtbl.add missing_tab tag ()
         end;
       deflt
diff --git a/library/libobject.mli b/library/libobject.mli
index c0d89e4d..57c3debe 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -1,30 +1,26 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libobject.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Libnames
 open Mod_subst
-(*i*)
 
-(* [Libobject] declares persistent objects, given with methods:
+(** [Libobject] declares persistent objects, given with methods:
 
    * a caching function specifying how to add the object in the current
      scope;
      If the object wishes to register its visibility in the Nametab,
-     it should do so for all possible sufixes.
+     it should do so for all possible suffixes.
 
    * a loading function, specifying what to do when the module
      containing the object is loaded;
      If the object wishes to register its visibility in the Nametab,
-     it should do so for all sufixes no shorter than the "int" argument
+     it should do so for all suffixes no shorter than the "int" argument
 
    * an opening function, specifying what to do when the module
      containing the object is opened (imported);
@@ -39,7 +35,7 @@ open Mod_subst
                   the module name must be updated
      Keep       - the object is not substitutive, but survives module
                   closing
-     Anticipate - this is for objects that have to be explicitely
+     Anticipate - this is for objects that have to be explicitly
                   managed by the [end_module] function (like Require
                   and Read markers)
 
@@ -74,7 +70,7 @@ type 'a object_declaration = {
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
-(* The default object is a "Keep" object with empty methods.
+(** The default object is a "Keep" object with empty methods.
    Object creators are advised to use the construction
    [{(default_object "MY_OBJECT") with
       cache_function = ...
@@ -85,18 +81,22 @@ type 'a object_declaration = {
 
 val default_object : string -> 'a object_declaration
 
-(* the identity substitution function *)
+(** the identity substitution function *)
 val ident_subst_function : substitution * 'a -> 'a
 
-(*s Given an object declaration, the function [declare_object]
+(** {6 ... } *)
+(** Given an object declaration, the function [declare_object_full]
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
 
 type obj
 
-val declare_object :
+val declare_object_full :
   'a object_declaration -> ('a -> obj) * (obj -> 'a)
 
+val declare_object :
+  'a object_declaration -> ('a -> obj)
+
 val object_tag : obj -> string
 
 val cache_object : object_name * obj -> unit
diff --git a/library/library.ml b/library/library.ml
index 09f92e6a..37622874 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
 open Util
 
@@ -68,8 +66,6 @@ let add_load_path isroot (phys_path,coq_path) =
 	  load_paths := (phys_path,coq_path,isroot) :: !load_paths;
       | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
-let physical_paths (dp,lp) = dp
-
 let extend_path_with_dirpath p dir =
   List.fold_left Filename.concat p
     (List.map string_of_id (List.rev (repr_dirpath dir)))
@@ -119,7 +115,7 @@ type compilation_unit_name = dir_path
 
 type library_disk = {
   md_name : compilation_unit_name;
-  md_compiled : compiled_library;
+  md_compiled : LightenLibrary.lightened_compiled_library;
   md_objects : Declaremods.library_objects;
   md_deps : (compilation_unit_name * Digest.t) list;
   md_imports : compilation_unit_name list }
@@ -215,9 +211,6 @@ let library_is_loaded dir =
 let library_is_opened dir =
   List.exists (fun m -> m.library_name = dir) !libraries_imports_list
 
-let library_is_exported dir =
-  List.exists (fun m -> m.library_name = dir) !libraries_exports_list
-
 let loaded_libraries () =
   List.map (fun m -> m.library_name) !libraries_loaded_list
 
@@ -307,7 +300,7 @@ let subst_import (_,o) = o
 let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
 
-let (in_import, out_import) =
+let in_import : dir_path * bool -> obj =
   declare_object {(default_object "IMPORT LIBRARY") with
        cache_function = cache_import;
        open_function = open_import;
@@ -389,24 +382,41 @@ let try_locate_qualified_library (loc,qid) =
 (************************************************************************)
 (* Internalise libraries *)
 
-let lighten_library m =
-  if !Flags.dont_load_proofs then lighten_library m else m
-
-let mk_library md digest = {
-  library_name = md.md_name;
-  library_compiled = lighten_library md.md_compiled;
-  library_objects = md.md_objects;
-  library_deps = md.md_deps;
-  library_imports = md.md_imports;
-  library_digest = digest }
+let mk_library md table digest =
+  let md_compiled =
+    LightenLibrary.load ~load_proof:!Flags.load_proofs table md.md_compiled
+  in {
+    library_name     = md.md_name;
+    library_compiled = md_compiled;
+    library_objects  = md.md_objects;
+    library_deps     = md.md_deps;
+    library_imports  = md.md_imports;
+    library_digest    = digest
+  }
+
+let fetch_opaque_table (f,pos,digest) =
+  try
+    let ch = System.with_magic_number_check raw_intern_library f in
+    seek_in ch pos;
+    if System.marshal_in ch <> digest then failwith "File changed!";
+    let table = (System.marshal_in ch : LightenLibrary.table) in
+    close_in ch;
+    table
+  with _ ->
+    error
+      ("The file "^f^" is inaccessible or has changed,\n" ^
+       "cannot load some opaque constant bodies in it.\n")
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
-  let md = System.marshal_in ch in
+  let lmd = System.marshal_in ch in
+  let pos = pos_in ch in
   let digest = System.marshal_in ch in
+  let table = lazy (fetch_opaque_table (f,pos,digest)) in
+  register_library_filename lmd.md_name f;
+  let library = mk_library lmd table digest in
   close_in ch;
-  register_library_filename md.md_name f;
-  mk_library md digest
+  library
 
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
@@ -453,9 +463,9 @@ let rec_intern_by_filename_only id f =
   (* We check no other file containing same library is loaded *)
   if library_is_loaded m.library_name then
     begin
-      Flags.if_verbose warning
-	((string_of_dirpath m.library_name)^" is already loaded from file "^
-	library_full_filename m.library_name);
+      Flags.if_warn msg_warning
+	(pr_dirpath m.library_name ++ str " is already loaded from file " ++
+	str (library_full_filename m.library_name));
       m.library_name, []
     end
  else
@@ -488,7 +498,7 @@ let rec_intern_library_from_file idopt f =
 
 type library_reference = dir_path list * bool option
 
-let register_library (dir,m) =
+let register_library m =
   Declaremods.register_library
     m.library_name
     m.library_compiled
@@ -516,7 +526,9 @@ let discharge_require (_,o) = Some o
 
 (* open_function is never called from here because an Anticipate object *)
 
-let (in_require, out_require) =
+type require_obj = library_t list * dir_path list * bool option
+
+let in_require : require_obj -> obj =
   declare_object {(default_object "REQUIRE") with
        cache_function = cache_require;
        load_function = load_require;
@@ -531,9 +543,10 @@ let xml_require = ref (fun d -> ())
 let set_xml_require f = xml_require := f
 
 let require_library_from_dirpath modrefl export =
-  let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
+  let needed = List.fold_left rec_intern_library [] modrefl in
+  let needed = List.rev_map snd needed in
   let modrefl = List.map fst modrefl in
-    if Lib.is_modtype () || Lib.is_module () then
+    if Lib.is_module_or_modtype () then
       begin
 	add_anonymous_leaf (in_require (needed,modrefl,None));
 	Option.iter (fun exp ->
@@ -551,8 +564,8 @@ let require_library qidl export =
 
 let require_library_from_file idopt file export =
   let modref,needed = rec_intern_library_from_file idopt file in
-  let needed = List.rev needed in
-  if Lib.is_modtype () || Lib.is_module () then begin
+  let needed = List.rev_map snd needed in
+  if Lib.is_module_or_modtype () then begin
     add_anonymous_leaf (in_require (needed,[modref],None));
     Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
       export
@@ -568,7 +581,7 @@ let import_module export (loc,qid) =
   try
     match Nametab.locate_module qid with
       | MPfile dir ->
-	  if Lib.is_modtype () || Lib.is_module () || not export then
+	  if Lib.is_module_or_modtype () || not export then
 	    add_anonymous_leaf (in_import (dir, export))
 	  else
 	    add_anonymous_leaf (in_import (dir, export))
@@ -620,6 +633,7 @@ let error_recursively_dependent_library dir =
    writing the content and computing the checksum... *)
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
+  let cenv, table = LightenLibrary.save cenv in
   let md = {
     md_name = dir;
     md_compiled = cenv;
@@ -632,8 +646,14 @@ let save_library_to dir f =
   try
     System.marshal_out ch md;
     flush ch;
+    (* The loading of the opaque definitions table is optional whereas
+       the digest is loaded all the time. As a consequence, the digest
+       must be serialized before the table (if we want to keep the
+       current simple layout of .vo files). This also entails that the
+       digest does not take opaque terms into account anymore. *)
     let di = Digest.file f' in
     System.marshal_out ch di;
+    System.marshal_out ch table;
     close_out ch
   with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e
 
diff --git a/library/library.mli b/library/library.mli
index bc939666..ed17ed15 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -1,21 +1,17 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: library.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Util
 open Names
 open Libnames
 open Libobject
-(*i*)
 
-(*s This module provides functions to load, open and save
+(** This module provides functions to load, open and save
   libraries. Libraries correspond to the subclass of modules that
   coincide with a file on disk (the ".vo" files). Libraries on the
   disk comes with checksums (obtained with the [Digest] module), which
@@ -23,43 +19,46 @@ open Libobject
   written at various dates.
 *)
 
-(*s Require = load in the environment + open (if the optional boolean
+(** {6 ... } *)
+(** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library : qualid located list -> bool option -> unit
 val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit
 val require_library_from_file :
   identifier option -> System.physical_path -> bool option -> unit
 
-(*s Open a module (or a library); if the boolean is true then it's also
+(** {6 ... } *)
+(** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located -> unit
 
-(*s Start the compilation of a library *)
+(** {6 Start the compilation of a library } *)
 val start_library : string -> dir_path * string
 
-(*s End the compilation of a library and save it to a ".vo" file *)
+(** {6 End the compilation of a library and save it to a ".vo" file } *)
 val save_library_to : dir_path -> string -> unit
 
-(*s Interrogate the status of libraries *)
+(** {6 Interrogate the status of libraries } *)
 
-  (* - Tell if a library is loaded or opened *)
+  (** - Tell if a library is loaded or opened *)
 val library_is_loaded : dir_path -> bool
 val library_is_opened : dir_path -> bool
 
-  (* - Tell which libraries are loaded or imported *)
+  (** - Tell which libraries are loaded or imported *)
 val loaded_libraries : unit -> dir_path list
 val opened_libraries : unit -> dir_path list
 
-  (* - Return the full filename of a loaded library. *)
+  (** - Return the full filename of a loaded library. *)
 val library_full_filename : dir_path -> string
 
-  (* - Overwrite the filename of all libraries (used when restoring a state) *)
+  (** - Overwrite the filename of all libraries (used when restoring a state) *)
 val overwrite_library_filenames : string -> unit
 
-(*s Hook for the xml exportation of libraries *)
+(** {6 Hook for the xml exportation of libraries } *)
 val set_xml_require : (dir_path -> unit) -> unit
 
-(*s Global load paths: a load path is a physical path in the file
+(** {6 ... } *)
+(** Global load paths: a load path is a physical path in the file
     system; to each load path is associated a Coq [dir_path] (the "logical"
     path of the physical path) *)
 
@@ -70,7 +69,7 @@ val remove_load_path : System.physical_path -> unit
 val find_logical_path : System.physical_path -> dir_path
 val is_in_load_paths : System.physical_path -> bool
 
-(*s Locate a library in the load paths *)
+(** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
@@ -79,5 +78,5 @@ val locate_qualified_library :
   bool -> qualid -> library_location * dir_path * System.physical_path
 val try_locate_qualified_library : qualid located -> dir_path * string
 
-(*s Statistics: display the memory use of a library. *)
+(** {6 Statistics: display the memory use of a library. } *)
 val mem : dir_path -> Pp.std_ppcmds
diff --git a/library/nameops.ml b/library/nameops.ml
index 6a4bec5a..799b8ebe 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
 open Util
 open Names
@@ -112,8 +110,6 @@ let add_prefix s id = id_of_string (s ^ string_of_id id)
 
 let atompart_of_id id = fst (repr_ident id)
 
-let lift_ident = lift_subscript
-
 (* Names *)
 
 let out_name = function
diff --git a/library/nameops.mli b/library/nameops.mli
index e549d506..f3f9f752 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -1,24 +1,22 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nameops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Names
 
-(* Identifiers and names *)
+(** Identifiers and names *)
 val pr_id : identifier -> Pp.std_ppcmds
 val pr_name : name -> Pp.std_ppcmds
 
 val make_ident : string -> int option -> identifier
 val repr_ident : identifier -> string * int option
 
-val atompart_of_id : identifier -> string  (* remove trailing digits *)
-val root_of_id : identifier -> identifier (* remove trailing digits, $'$ and $\_$ *)
+val atompart_of_id : identifier -> string  (** remove trailing digits *)
+val root_of_id : identifier -> identifier (** remove trailing digits, ' and _ *)
 
 val add_suffix : identifier -> string -> identifier
 val add_prefix : string -> identifier -> identifier
@@ -38,17 +36,17 @@ val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a *
 
 val pr_lab : label -> Pp.std_ppcmds
 
-(* some preset paths *)
+(** some preset paths *)
 
 val default_library : dir_path
 
-(* This is the root of the standard library of Coq *)
+(** This is the root of the standard library of Coq *)
 val coq_root : module_ident
 
-(* This is the default root prefix for developments which doesn't
+(** This is the default root prefix for developments which doesn't
    mention a root *)
 val default_root_prefix : dir_path
 
-(* Metavariables *)
+(** Metavariables *)
 val pr_meta : Term.metavariable -> Pp.std_ppcmds
 val string_of_meta : Term.metavariable -> string
diff --git a/library/nametab.ml b/library/nametab.ml
index c4ea5953..6dbd927d 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -1,14 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nametab.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
+open Compat
 open Pp
 open Names
 open Libnames
@@ -20,10 +19,10 @@ exception GlobalizationError of qualid
 exception GlobalizationConstantError of qualid
 
 let error_global_not_found_loc loc q =
-  Stdpp.raise_with_loc loc (GlobalizationError q)
+  Loc.raise loc (GlobalizationError q)
 
 let error_global_constant_not_found_loc loc q =
-  Stdpp.raise_with_loc loc (GlobalizationConstantError q)
+  Loc.raise loc (GlobalizationConstantError q)
 
 let error_global_not_found q = raise (GlobalizationError q)
 
@@ -109,9 +108,9 @@ struct
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-		  Flags.if_verbose
-		    warning ("Trying to mask the absolute name \""
-			     ^ U.to_string n ^ "\"!");
+		  Flags.if_warn
+		    msg_warning (str ("Trying to mask the absolute name \""
+			     ^ U.to_string n ^ "\"!"));
 		  current
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
@@ -132,7 +131,7 @@ struct
 		   become unaccessible forever *)
 		(* But ours is also absolute! This is an error! *)
 		error ("Cannot mask the absolute name \""
-  		       ^ U.to_string uname' ^ "\"!")
+		       ^ U.to_string uname' ^ "\"!")
 	  | Nothing
 	  | Relative _ -> Absolute (uname,o), dirmap
 
@@ -149,9 +148,9 @@ let rec push_exactly uname o level (current,dirmap) = function
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-		  Flags.if_verbose
-		    warning ("Trying to mask the absolute name \""
-  			     ^ U.to_string n ^ "\"!");
+		  Flags.if_warn
+		    msg_warning (str ("Trying to mask the absolute name \""
+			     ^ U.to_string n ^ "\"!"));
 		  current
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
@@ -288,10 +287,7 @@ let the_dirtab = ref (DirTab.empty : dirtab)
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
-module Globrevtab = Map.Make(struct
-			       type t=extended_global_reference
-			       let compare = compare
-			     end)
+module Globrevtab = Map.Make(ExtRefOrdered)
 
 type globrevtab = full_path Globrevtab.t
 let the_globrevtab = ref (Globrevtab.empty : globrevtab)
@@ -379,7 +375,6 @@ let locate_modtype qid = SpTab.locate qid !the_modtypetab
 let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
 
 let locate_tactic qid = SpTab.locate qid !the_tactictab
-let full_name_tactic qid = SpTab.user_name qid !the_tactictab
 
 let locate_dir qid = DirTab.locate qid !the_dirtab
 
@@ -412,11 +407,6 @@ let locate_constant qid =
     | TrueGlobal (ConstRef kn) -> kn
     | _ -> raise Not_found
 
-let locate_mind qid =
-  match locate_extended qid with
-    | TrueGlobal (IndRef (kn,0)) -> kn
-    | _ -> raise Not_found
-
 let global_of_path sp =
   match SpTab.find sp !the_ccitab with
     | TrueGlobal ref -> ref
@@ -424,9 +414,6 @@ let global_of_path sp =
 
 let extended_global_of_path sp = SpTab.find sp !the_ccitab
 
-let locate_in_absolute_module dir id =
-  global_of_path (make_path dir id)
-
 let global r =
   let (loc,qid) = qualid_of_reference r in
   try match locate_extended qid with
@@ -450,8 +437,6 @@ let exists_module = exists_dir
 
 let exists_modtype sp = SpTab.exists sp !the_modtypetab
 
-let exists_tactic sp = SpTab.exists sp !the_tactictab
-
 (* Reverse locate functions ***********************************************)
 
 let path_of_global ref =
diff --git a/library/nametab.mli b/library/nametab.mli
index d0c24bfa..c5b55f2c 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -1,86 +1,78 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nametab.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Util
 open Pp
 open Names
 open Libnames
-(*i*)
 
-(*s This module contains the tables for globalization, which
-    associates internal object references to qualified names (qualid).
+(** This module contains the tables for globalization. *)
 
-    There are three classes of names:
+(** These globalization tables associate internal object references to
+    qualified names (qualid). There are three classes of names:
 
-    1a- internal kernel names: [kernel_name], [constant], [inductive],
-        [module_path], [dir_path]
+    - 1a) internal kernel names: [kernel_name], [constant], [inductive],
+         [module_path], [dir_path]
 
-    1b- other internal names: [global_reference], [syndef_name],
+    - 1b) other internal names: [global_reference], [syndef_name],
         [extended_global_reference], [global_dir_reference], ...
 
-    2- full, non ambiguous user names: [full_path]
+    - 2) full, non ambiguous user names: [full_path]
 
-    3- non necessarily full, possibly ambiguous user names: [reference]
-       and [qualid]
+    - 3) non necessarily full, possibly ambiguous user names: [reference]
+        and [qualid]
 *)
 
-(* Most functions in this module fall into one of the following categories:
-   \begin{itemize}
-   \item [push : visibility -> full_user_name -> object_reference -> unit]
-
-   Registers the [object_reference] to be referred to by the
-   [full_user_name] (and its suffixes according to [visibility]).
-   [full_user_name] can either be a [full_path] or a [dir_path].
-
-   \item [exists : full_user_name -> bool]
+(** Most functions in this module fall into one of the following categories:
+{ul {- [push : visibility -> full_user_name -> object_reference -> unit]
 
-   Is the [full_user_name] already atributed as an absolute user name
-   of some object?
+     Registers the [object_reference] to be referred to by the
+     [full_user_name] (and its suffixes according to [visibility]).
+     [full_user_name] can either be a [full_path] or a [dir_path].
+   }
+   {- [exists : full_user_name -> bool]
 
-   \item [locate : qualid -> object_reference]
+     Is the [full_user_name] already atributed as an absolute user name
+     of some object?
+   }
+   {- [locate : qualid -> object_reference]
 
-   Finds the object referred to by [qualid] or raises [Not_found]
+     Finds the object referred to by [qualid] or raises [Not_found]
+   }
+   {- [full_name : qualid -> full_user_name]
 
-   \item [full_name : qualid -> full_user_name]
+     Finds the full user name referred to by [qualid] or raises [Not_found]
+   }
+   {- [shortest_qualid_of : object_reference -> user_name]
 
-   Finds the full user name referred to by [qualid] or raises [Not_found]
+     The [user_name] can be for example the shortest non ambiguous [qualid] or
+     the [full_user_name] or [identifier]. Such a function can also have a
+     local context argument.}}
 
-   \item [shortest_qualid_of : object_reference -> user_name]
-
-   The [user_name] can be for example the shortest non ambiguous [qualid] or
-   the [full_user_name] or [identifier]. Such a function can also have a
-   local context argument.
-   \end{itemize}
 *)
 
 
 exception GlobalizationError of qualid
 exception GlobalizationConstantError of qualid
 
-(* Raises a globalization error *)
+(** Raises a globalization error *)
 val error_global_not_found_loc : loc -> qualid -> 'a
 val error_global_not_found     : qualid -> 'a
 val error_global_constant_not_found_loc : loc -> qualid -> 'a
 
-(*s Register visibility of things *)
-
-(* The visibility can be registered either
-   \begin{itemize}
+(** {6 Register visibility of things } *)
 
-   \item for all suffixes not shorter then a given int -- when the
+(** The visibility can be registered either
+   - for all suffixes not shorter then a given int -- when the
    object is loaded inside a module -- or
-
-   \item for a precise suffix, when the module containing (the module
+   - for a precise suffix, when the module containing (the module
    containing ...) the object is opened (imported)
-   \end{itemize}
+   
 *)
 
 type visibility = Until of int | Exactly of int
@@ -94,9 +86,9 @@ type ltac_constant = kernel_name
 val push_tactic : visibility -> full_path -> ltac_constant -> unit
 
 
-(*s The following functions perform globalization of qualified names *)
+(** {6 The following functions perform globalization of qualified names } *)
 
-(* These functions globalize a (partially) qualified name or fail with
+(** These functions globalize a (partially) qualified name or fail with
    [Not_found] *)
 
 val locate : qualid -> global_reference
@@ -109,42 +101,43 @@ val locate_module : qualid -> module_path
 val locate_section : qualid -> dir_path
 val locate_tactic : qualid -> ltac_constant
 
-(* These functions globalize user-level references into global
+(** These functions globalize user-level references into global
    references, like [locate] and co, but raise a nice error message
    in case of failure *)
 
 val global : reference -> global_reference
 val global_inductive : reference -> inductive
 
-(* These functions locate all global references with a given suffix;
+(** These functions locate all global references with a given suffix;
    if [qualid] is valid as such, it comes first in the list *)
 
 val locate_all : qualid -> global_reference list
 val locate_extended_all : qualid -> extended_global_reference list
 
-(* Mapping a full path to a global reference *)
+(** Mapping a full path to a global reference *)
 
 val global_of_path : full_path -> global_reference
 val extended_global_of_path : full_path -> extended_global_reference
 
-(*s These functions tell if the given absolute name is already taken *)
+(** {6 These functions tell if the given absolute name is already taken } *)
 
 val exists_cci : full_path -> bool
 val exists_modtype : full_path -> bool
 val exists_dir : dir_path -> bool
-val exists_section : dir_path -> bool (* deprecated synonym of [exists_dir] *)
-val exists_module : dir_path -> bool (* deprecated synonym of [exists_dir] *)
+val exists_section : dir_path -> bool (** deprecated synonym of [exists_dir] *)
+val exists_module : dir_path -> bool (** deprecated synonym of [exists_dir] *)
 
-(*s These functions locate qualids into full user names *)
+(** {6 These functions locate qualids into full user names } *)
 
 val full_name_cci : qualid -> full_path
 val full_name_modtype : qualid -> full_path
 val full_name_module : qualid -> dir_path
 
-(*s Reverse lookup -- finding user names corresponding to the given
+(** {6 Reverse lookup }
+  Finding user names corresponding to the given
   internal name *)
 
-(* Returns the full path bound to a global reference or syntactic
+(** Returns the full path bound to a global reference or syntactic
    definition, and the (full) dirpath associated to a module path *)
 
 val path_of_syndef : syndef_name -> full_path
@@ -152,17 +145,17 @@ val path_of_global : global_reference -> full_path
 val dirpath_of_module : module_path -> dir_path
 val path_of_tactic : ltac_constant -> full_path
 
-(* Returns in particular the dirpath or the basename of the full path
+(** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
 
 val dirpath_of_global : global_reference -> dir_path
 val basename_of_global : global_reference -> identifier
 
-(* Printing of global references using names as short as possible *)
+(** Printing of global references using names as short as possible *)
 val pr_global_env : Idset.t -> global_reference -> std_ppcmds
 
 
-(* The [shortest_qualid] functions given an object with [user_name]
+(** The [shortest_qualid] functions given an object with [user_name]
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
    Coq.A.B.x that denotes the same object. *)
 
@@ -172,7 +165,7 @@ val shortest_qualid_of_modtype : module_path -> qualid
 val shortest_qualid_of_module : module_path -> qualid
 val shortest_qualid_of_tactic : ltac_constant -> qualid
 
-(* Deprecated synonyms *)
+(** Deprecated synonyms *)
 
 val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
-val absolute_reference : full_path -> global_reference (* = global_of_path *)
+val absolute_reference : full_path -> global_reference (** = global_of_path *)
diff --git a/library/states.ml b/library/states.ml
index 679f9028..c88858f7 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open System
 
 type state = Lib.frozen * Summary.frozen
@@ -22,7 +20,10 @@ let unfreeze (fl,fs) =
 let (extern_state,intern_state) =
   let (raw_extern, raw_intern) =
     extern_intern Coq_config.state_magic_number ".coq" in
-  (fun s -> raw_extern s (freeze())),
+  (fun s ->
+    if !Flags.load_proofs <> Flags.Force then
+      Util.error "Write State only works with option -force-load-proofs";
+    raw_extern s (freeze())),
   (fun s ->
     unfreeze
       (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
diff --git a/library/states.mli b/library/states.mli
index fc6497b6..4f114d57 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -1,14 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: states.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** {6 States of the system} *)
 
-(*s States of the system. In that module, we provide functions to get
+(** In that module, we provide functions to get
   and set the state of the whole system. Internally, it is done by
   freezing the states of both [Lib] and [Summary]. We provide functions
   to write and restore state to and from a given file. *)
@@ -20,13 +20,14 @@ type state
 val freeze : unit -> state
 val unfreeze : state -> unit
 
-(*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the
+(** {6 Rollback } *)
+
+(** [with_heavy_rollback f x] applies [f] to [x] and restores the
   state of the whole system as it was before the evaluation if an exception
   is raised. *)
-
 val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
 
-(*s [with_state_protection f x] applies [f] to [x] and restores the
+(** [with_state_protection f x] applies [f] to [x] and restores the
   state of the whole system as it was before the evaluation of f *)
 
 val with_state_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/library/summary.ml b/library/summary.ml
index a40a9354..697f57e8 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $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 5db9617b..5963b23b 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*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
+(** This module registers the declaration of global tables, which will be kept
    in synchronization during the various backtracks of the system. *)
 
 type 'a summary_declaration = {