Imported Upstream version 8.9.0upstream/8.9.0upstream

27 files changed, 436 insertions, 697 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 3f01c617..408e2591 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -171,16 +171,16 @@ let jmeq_kn = make_ind jmeq_module "JMeq"
 let glob_jmeq = IndRef (jmeq_kn,0)
 
 type coq_sigma_data = {
-  proj1 : global_reference;
-  proj2 : global_reference;
-  elim  : global_reference;
-  intro : global_reference;
-  typ   : global_reference }
+  proj1 : GlobRef.t;
+  proj2 : GlobRef.t;
+  elim  : GlobRef.t;
+  intro : GlobRef.t;
+  typ   : GlobRef.t }
 
 type coq_bool_data  = {
-  andb : global_reference;
-  andb_prop : global_reference;
-  andb_true_intro : global_reference}
+  andb : GlobRef.t;
+  andb_prop : GlobRef.t;
+  andb_true_intro : GlobRef.t}
 
 let build_bool_type () =
   { andb =  init_reference ["Datatypes"] "andb";
@@ -213,18 +213,18 @@ let build_prod () =
 
 (* Equalities *)
 type coq_eq_data = {
-  eq   : global_reference;
-  ind  : global_reference;
-  refl : global_reference;
-  sym  : global_reference;
-  trans: global_reference;
-  congr: global_reference }
+  eq   : GlobRef.t;
+  ind  : GlobRef.t;
+  refl : GlobRef.t;
+  sym  : GlobRef.t;
+  trans: GlobRef.t;
+  congr: GlobRef.t }
 
 (* Data needed for discriminate and injection *)
 type coq_inversion_data = {
-  inv_eq   : global_reference; (* : forall params, t -> Prop *)
-  inv_ind  : global_reference; (* : forall params P y, eq params y -> P y *)
-  inv_congr: global_reference  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+  inv_eq   : GlobRef.t; (* : forall params, t -> Prop *)
+  inv_ind  : GlobRef.t; (* : forall params P y, eq params y -> P y *)
+  inv_congr: GlobRef.t  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
 }
 
 let lazy_init_reference dir id = lazy (init_reference dir id)
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 8077c47c..b4bd1b0e 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -8,10 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Names
 open Libnames
-open Globnames
-open Util
 
 (** This module collects the global references, constructions and
     patterns of the standard library used in ocaml files *)
@@ -44,14 +43,14 @@ open Util
 
 type message = string
 
-val find_reference : message -> string list -> string -> global_reference
-val coq_reference : message -> string list -> string -> global_reference
+val find_reference : message -> string list -> string -> GlobRef.t
+val coq_reference : message -> string list -> string -> GlobRef.t
 
 (** For tactics/commands requiring vernacular libraries *)
 val check_required_library : string list -> unit
 
 (** Search in several modules (not prefixed by "Coq") *)
-val gen_reference_in_modules : string->string list list-> string -> global_reference
+val gen_reference_in_modules : string->string list list-> string -> GlobRef.t
 
 val arith_modules : string list list
 val zarith_base_modules : string list list
@@ -78,24 +77,24 @@ val type_of_id : Constant.t
 
 (** Natural numbers *)
 val nat_path : full_path
-val glob_nat : global_reference
+val glob_nat : GlobRef.t
 val path_of_O : constructor
 val path_of_S : constructor
-val glob_O : global_reference
-val glob_S : global_reference
+val glob_O : GlobRef.t
+val glob_S : GlobRef.t
 
 (** Booleans *)
-val glob_bool : global_reference
+val glob_bool : GlobRef.t
 val path_of_true : constructor
 val path_of_false : constructor
-val glob_true : global_reference
-val glob_false : global_reference
+val glob_true : GlobRef.t
+val glob_false : GlobRef.t
 
 
 (** Equality *)
-val glob_eq : global_reference
-val glob_identity : global_reference
-val glob_jmeq : global_reference
+val glob_eq : GlobRef.t
+val glob_identity : GlobRef.t
+val glob_jmeq : GlobRef.t
 
 (** {6 ... } *)
 (** Constructions and patterns related to Coq initial state are unknown
@@ -106,18 +105,18 @@ val glob_jmeq : global_reference
    at runtime. *)
 
 type coq_bool_data = {
-  andb : global_reference;
-  andb_prop : global_reference;
-  andb_true_intro : global_reference}
+  andb : GlobRef.t;
+  andb_prop : GlobRef.t;
+  andb_true_intro : GlobRef.t}
 val build_bool_type : coq_bool_data delayed
 
 (** {6 For Equality tactics } *)
 type coq_sigma_data = {
-  proj1 : global_reference;
-  proj2 : global_reference;
-  elim  : global_reference;
-  intro : global_reference;
-  typ   : global_reference }
+  proj1 : GlobRef.t;
+  proj2 : GlobRef.t;
+  elim  : GlobRef.t;
+  intro : GlobRef.t;
+  typ   : GlobRef.t }
 
 val build_sigma_set : coq_sigma_data delayed
 val build_sigma_type : coq_sigma_data delayed
@@ -132,30 +131,30 @@ val build_sigma : coq_sigma_data delayed
 val build_prod : coq_sigma_data delayed
 
 type coq_eq_data = {
-  eq   : global_reference;
-  ind  : global_reference;
-  refl : global_reference;
-  sym  : global_reference;
-  trans: global_reference;
-  congr: global_reference }
+  eq   : GlobRef.t;
+  ind  : GlobRef.t;
+  refl : GlobRef.t;
+  sym  : GlobRef.t;
+  trans: GlobRef.t;
+  congr: GlobRef.t }
 
 val build_coq_eq_data : coq_eq_data delayed
 
 val build_coq_identity_data : coq_eq_data delayed
 val build_coq_jmeq_data : coq_eq_data delayed
 
-val build_coq_eq       : global_reference delayed (** = [(build_coq_eq_data()).eq] *)
-val build_coq_eq_refl  : global_reference delayed (** = [(build_coq_eq_data()).refl] *)
-val build_coq_eq_sym   : global_reference delayed (** = [(build_coq_eq_data()).sym] *)
-val build_coq_f_equal2 : global_reference delayed
+val build_coq_eq       : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq_refl  : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *)
+val build_coq_eq_sym   : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *)
+val build_coq_f_equal2 : GlobRef.t delayed
 
 (** Data needed for discriminate and injection *)
 
 type coq_inversion_data = {
-  inv_eq   : global_reference; (** : forall params, args -> Prop *)
-  inv_ind  : global_reference; (** : forall params P (H : P params) args, eq params args 
+  inv_eq   : GlobRef.t; (** : forall params, args -> Prop *)
+  inv_ind  : GlobRef.t; (** : forall params P (H : P params) args, eq params args
 			 ->  P args *)
-  inv_congr: global_reference  (** : forall params B (f:t->B) args, eq params args -> 
+  inv_congr: GlobRef.t  (** : forall params B (f:t->B) args, eq params args ->
 			 f params = f args *)
 }
 
@@ -165,45 +164,45 @@ val build_coq_inversion_jmeq_data : coq_inversion_data delayed
 val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 
 (** Specif *)
-val build_coq_sumbool : global_reference delayed
+val build_coq_sumbool : GlobRef.t delayed
 
 (** {6 ... } *)
 (** Connectives 
    The False proposition *)
-val build_coq_False : global_reference delayed
+val build_coq_False : GlobRef.t delayed
 
 (** The True proposition and its unique proof *)
-val build_coq_True : global_reference delayed
-val build_coq_I : global_reference delayed
+val build_coq_True : GlobRef.t delayed
+val build_coq_I : GlobRef.t delayed
 
 (** Negation *)
-val build_coq_not : global_reference delayed
+val build_coq_not : GlobRef.t delayed
 
 (** Conjunction *)
-val build_coq_and : global_reference delayed
-val build_coq_conj : global_reference delayed
-val build_coq_iff : global_reference delayed
+val build_coq_and : GlobRef.t delayed
+val build_coq_conj : GlobRef.t delayed
+val build_coq_iff : GlobRef.t delayed
 
-val build_coq_iff_left_proj : global_reference delayed
-val build_coq_iff_right_proj : global_reference delayed
+val build_coq_iff_left_proj : GlobRef.t delayed
+val build_coq_iff_right_proj : GlobRef.t delayed
 
 (** Disjunction *)
-val build_coq_or : global_reference delayed
+val build_coq_or : GlobRef.t delayed
 
 (** Existential quantifier *)
-val build_coq_ex : global_reference delayed
-
-val coq_eq_ref : global_reference lazy_t
-val coq_identity_ref : global_reference lazy_t
-val coq_jmeq_ref : global_reference lazy_t
-val coq_eq_true_ref : global_reference lazy_t
-val coq_existS_ref : global_reference lazy_t
-val coq_existT_ref : global_reference lazy_t
-val coq_exist_ref : global_reference lazy_t
-val coq_not_ref : global_reference lazy_t
-val coq_False_ref : global_reference lazy_t
-val coq_sumbool_ref : global_reference lazy_t
-val coq_sig_ref : global_reference lazy_t
-
-val coq_or_ref : global_reference lazy_t
-val coq_iff_ref : global_reference lazy_t
+val build_coq_ex : GlobRef.t delayed
+
+val coq_eq_ref : GlobRef.t lazy_t
+val coq_identity_ref : GlobRef.t lazy_t
+val coq_jmeq_ref : GlobRef.t lazy_t
+val coq_eq_true_ref : GlobRef.t lazy_t
+val coq_existS_ref : GlobRef.t lazy_t
+val coq_existT_ref : GlobRef.t lazy_t
+val coq_exist_ref : GlobRef.t lazy_t
+val coq_not_ref : GlobRef.t lazy_t
+val coq_False_ref : GlobRef.t lazy_t
+val coq_sumbool_ref : GlobRef.t lazy_t
+val coq_sig_ref : GlobRef.t lazy_t
+
+val coq_or_ref : GlobRef.t lazy_t
+val coq_iff_ref : GlobRef.t lazy_t
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
new file mode 100644
index 00000000..c1a673ed
--- /dev/null
+++ b/library/decl_kinds.ml
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Informal mathematical status of declarations *)
+
+type discharge = DoDischarge | NoDischarge
+
+type locality = Discharge | Local | Global
+
+type binding_kind = Explicit | Implicit
+
+type polymorphic = bool
+
+type private_flag = bool
+
+type cumulative_inductive_flag = bool
+
+type theorem_kind =
+  | Theorem
+  | Lemma
+  | Fact
+  | Remark
+  | Property
+  | Proposition
+  | Corollary
+
+type definition_object_kind =
+  | Definition
+  | Coercion
+  | SubClass
+  | CanonicalStructure
+  | Example
+  | Fixpoint
+  | CoFixpoint
+  | Scheme
+  | StructureComponent
+  | IdentityCoercion
+  | Instance
+  | Method
+  | Let
+
+type assumption_object_kind = Definitional | Logical | Conjectural
+
+(* [assumption_kind]
+
+                |  Local      | Global
+   ------------------------------------
+   Definitional |  Variable   | Parameter
+   Logical      |  Hypothesis | Axiom
+
+*)
+type assumption_kind = locality * polymorphic * assumption_object_kind
+
+type definition_kind = locality * polymorphic * definition_object_kind
+
+(** Kinds used in proofs *)
+
+type goal_object_kind =
+  | DefinitionBody of definition_object_kind
+  | Proof of theorem_kind
+
+type goal_kind = locality * polymorphic * goal_object_kind
+
+(** Kinds used in library *)
+
+type logical_kind =
+  | IsAssumption of assumption_object_kind
+  | IsDefinition of definition_object_kind
+  | IsProof of theorem_kind
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 762efc5e..0b3b461e 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -17,11 +17,26 @@ open Entries
 open Libnames
 open Libobject
 open Mod_subst
-open Vernacexpr
-open Misctypes
 
 (** {6 Inlining levels} *)
 
+(** Rigid / flexible module signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Which module 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
+
+type module_kind = Module | ModType | ModAny
+
 let default_inline () = Some (Flags.get_inline_level ())
 
 let inl2intopt = function
@@ -980,8 +995,8 @@ let iter_all_segments f =
 (** {6 Some types used to shorten declaremods.mli} *)
 
 type 'modast module_interpretor =
-  Environ.env -> Misctypes.module_kind -> 'modast ->
-    Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
+  Environ.env -> module_kind -> 'modast ->
+    Entries.module_struct_entry * module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
   (lident list * ('modast * inline)) list
diff --git a/library/declaremods.mli b/library/declaremods.mli
index fd8d2961..b42a59bf 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -9,16 +9,34 @@
 (************************************************************************)
 
 open Names
-open Vernacexpr
 
 (** {6 Modules } *)
 
+(** Rigid / flexible module signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Which module 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
+
+(** Kinds of modules *)
+
+type module_kind = Module | ModType | ModAny
+
 type 'modast module_interpretor =
-  Environ.env -> Misctypes.module_kind -> 'modast ->
-    Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
+  Environ.env -> module_kind -> 'modast ->
+    Entries.module_struct_entry * module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
-  (Misctypes.lident list * ('modast * inline)) list
+  (lident list * ('modast * inline)) list
 
 (** [declare_module interp_modast id fargs typ exprs]
    declares module [id], with structure constructed by [interp_modast]
diff --git a/library/global.ml b/library/global.ml
index dcb20a28..e833f711 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -90,6 +90,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let typing_flags () = Environ.typing_flags (env ())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
@@ -278,3 +279,9 @@ let register_inline c = globalize0 (Safe_typing.register_inline c)
 let set_strategy k l =
   GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
 
+let set_reduction_sharing b =
+  let env = safe_env () in
+  let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in
+  let flags = { flags with Declarations.share_reduction = b } in
+  let env = Safe_typing.set_typing_flags flags env in
+  GlobalSafeEnv.set_safe_env env
diff --git a/library/global.mli b/library/global.mli
index b82039a0..2819c187 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -23,13 +23,14 @@ val env_is_initial : unit -> bool
 
 val universes : unit -> UGraph.t
 val named_context_val : unit -> Environ.named_context_val
-val named_context : unit -> Context.Named.t
+val named_context : unit -> Constr.named_context
 
 (** {6 Enriching the global environment } *)
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
+val typing_flags : unit -> Declarations.typing_flags
 
 (** Variables, Local definitions, constants, inductive types *)
 
@@ -79,7 +80,7 @@ val add_module_parameter :
 
 (** {6 Queries in the global environment } *)
 
-val lookup_named     : variable -> Context.Named.Declaration.t
+val lookup_named     : variable -> Constr.named_declaration
 val lookup_constant  : Constant.t -> Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
@@ -123,26 +124,26 @@ val env_of_context : Environ.named_context_val -> Environ.env
 val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
 val is_joined_environment : unit -> bool
 
-val is_polymorphic : Globnames.global_reference -> bool
-val is_template_polymorphic : Globnames.global_reference -> bool
-val is_type_in_type : Globnames.global_reference -> bool
+val is_polymorphic : GlobRef.t -> bool
+val is_template_polymorphic : GlobRef.t -> bool
+val is_type_in_type : GlobRef.t -> bool
 
 val constr_of_global_in_context : Environ.env ->
-  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+  GlobRef.t -> Constr.types * Univ.AUContext.t
 (** Returns the type of the constant in its local universe
     context. The type should not be used without pushing it's universe
     context in the environmnent of usage. For non-universe-polymorphic
     constants, it does not matter. *)
 
 val type_of_global_in_context : Environ.env -> 
-  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+  GlobRef.t -> Constr.types * Univ.AUContext.t
 (** Returns the type of the constant in its local universe
     context. The type should not be used without pushing it's universe
     context in the environmnent of usage. For non-universe-polymorphic
     constants, it does not matter. *)
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : Globnames.global_reference -> Univ.AUContext.t
+val universes_of_global : GlobRef.t -> Univ.AUContext.t
 
 (** {6 Retroknowledge } *)
 
@@ -155,6 +156,8 @@ val register_inline : Constant.t -> unit
 
 val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
+val set_reduction_sharing : bool -> unit
+
 (* Modifies the global state, registering new universes *)
 
 val current_modpath : unit -> ModPath.t
diff --git a/library/globnames.ml b/library/globnames.ml
index 6c9c813e..6383a1f8 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -15,7 +15,7 @@ open Mod_subst
 open Libnames
 
 (*s Global reference is a kernel side type for all references together *)
-type global_reference = Names.global_reference =
+type global_reference = GlobRef.t =
   | VarRef of variable           (** A reference to the section-context. *)
   | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
@@ -26,14 +26,6 @@ let isConstRef = function ConstRef _ -> true | _ -> false
 let isIndRef = function IndRef _ -> true | _ -> false
 let isConstructRef = function ConstructRef _ -> true | _ -> false
 
-let eq_gr gr1 gr2 =
-  gr1 == gr2 || match gr1,gr2 with
-    | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2
-    | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
-    | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
-    | VarRef v1, VarRef v2 -> Id.equal v1 v2
-    | _ -> false
-
 let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
 let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
@@ -95,8 +87,6 @@ let printable_constr_of_global = function
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
-let reference_of_constr = global_of_constr
-
 let global_eq_gen eq_cst eq_ind eq_cons x y =
   x == y ||
   match x, y with
@@ -245,3 +235,6 @@ let pop_global_reference = function
   | IndRef (kn,i) -> IndRef (pop_kn kn,i)
   | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
   | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
+
+(* Deprecated *)
+let eq_gr = GlobRef.equal
diff --git a/library/globnames.mli b/library/globnames.mli
index f2b88b87..15fcd5bd 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -14,71 +14,69 @@ open Constr
 open Mod_subst
 
 (** {6 Global reference is a kernel side type for all references together } *)
-type global_reference = Names.global_reference =
+type global_reference = GlobRef.t =
   | VarRef of variable           (** A reference to the section-context. *)
   | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
   | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
+[@@ocaml.deprecated "Use Names.GlobRef.t"]
 
-val isVarRef : global_reference -> bool
-val isConstRef : global_reference -> bool
-val isIndRef : global_reference -> bool
-val isConstructRef : global_reference -> bool
+val isVarRef : GlobRef.t -> bool
+val isConstRef : GlobRef.t -> bool
+val isIndRef : GlobRef.t -> bool
+val isConstructRef : GlobRef.t -> bool
 
-val eq_gr : global_reference -> global_reference -> bool
-val canonical_gr : global_reference -> global_reference
+val eq_gr : GlobRef.t -> GlobRef.t -> bool
+[@@ocaml.deprecated "Use Names.GlobRef.equal"]
+val canonical_gr : GlobRef.t -> GlobRef.t
 
-val destVarRef : global_reference -> variable
-val destConstRef : global_reference -> Constant.t
-val destIndRef : global_reference -> inductive
-val destConstructRef : global_reference -> constructor
+val destVarRef : GlobRef.t -> variable
+val destConstRef : GlobRef.t -> Constant.t
+val destIndRef : GlobRef.t -> inductive
+val destConstructRef : GlobRef.t -> constructor
 
-val is_global : global_reference -> constr -> bool
+val is_global : GlobRef.t -> constr -> bool
 
 val subst_constructor : substitution -> constructor -> constructor * constr
-val subst_global : substitution -> global_reference -> global_reference * constr
-val subst_global_reference : substitution -> global_reference -> global_reference
+val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr
+val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 
 (** This constr is not safe to be typechecked, universe polymorphism is not 
     handled here: just use for printing *)
-val printable_constr_of_global : global_reference -> constr
+val printable_constr_of_global : GlobRef.t -> constr
 
 (** 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 *)
-val reference_of_constr : constr -> global_reference
-[@@ocaml.deprecated "Alias of Globnames.global_of_constr"]
+val global_of_constr : constr -> GlobRef.t
 
 module RefOrdered : sig
-  type t = global_reference
+  type t = GlobRef.t
   val compare : t -> t -> int
   val equal : t -> t -> bool
   val hash : t -> int
 end
 
 module RefOrdered_env : sig
-  type t = global_reference
+  type t = GlobRef.t
   val compare : t -> t -> int
   val equal : t -> t -> bool
   val hash : t -> int
 end
 
-module Refset : CSig.SetS with type elt = global_reference
+module Refset : CSig.SetS with type elt = GlobRef.t
 module Refmap : Map.ExtS
-  with type key = global_reference and module Set := Refset
+  with type key = GlobRef.t and module Set := Refset
 
-module Refset_env : CSig.SetS with type elt = global_reference
+module Refset_env : CSig.SetS with type elt = GlobRef.t
 module Refmap_env : Map.ExtS
-  with type key = global_reference and module Set := Refset_env
+  with type key = GlobRef.t and module Set := Refset_env
 
 (** {6 Extended global references } *)
 
 type syndef_name = KerName.t
 
 type extended_global_reference =
-  | TrueGlobal of global_reference
+  | TrueGlobal of GlobRef.t
   | SynDef of syndef_name
 
 module ExtRefOrdered : sig
@@ -89,7 +87,7 @@ module ExtRefOrdered : sig
 end
 
 type global_reference_or_constr = 
-  | IsGlobal of global_reference
+  | IsGlobal of GlobRef.t
   | IsConstr of constr
 
 (** {6 Temporary function to brutally form kernel names from section paths } *)
@@ -100,7 +98,6 @@ val encode_con : DirPath.t -> Id.t -> Constant.t
 val decode_con : Constant.t -> DirPath.t * Id.t
 
 (** {6 Popping one level of section in global names } *)
-
 val pop_con : Constant.t -> Constant.t
 val pop_kn : MutInd.t-> MutInd.t
-val pop_global_reference : global_reference -> global_reference
+val pop_global_reference : GlobRef.t -> GlobRef.t
diff --git a/library/goptions.ml b/library/goptions.ml
index eb7bb5b4..dcbc46ab 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -161,7 +161,7 @@ module type RefConvertArg =
 sig
   type t
   val compare : t -> t -> int
-  val encode : reference -> t
+  val encode : qualid -> t
   val subst : substitution -> t -> t
   val printer : t -> Pp.t
   val key : option_name
@@ -172,7 +172,7 @@ end
 module RefConvert = functor (A : RefConvertArg) ->
 struct
   type t = A.t
-  type key = reference
+  type key = qualid
   let compare = A.compare
   let table = ref_table
   let encode = A.encode
@@ -318,26 +318,35 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v =
   | Some (name, depr, (read,write,append)) ->
     write locality (check_and_cast v (read ()))
 
-let bad_type_error () = user_err Pp.(str "Bad type of value for this option.")
+let show_value_type = function
+  | BoolValue _ -> "bool"
+  | IntValue _ -> "int"
+  | StringValue _ -> "string"
+  | StringOptValue _ -> "string"
+
+let bad_type_error opt_value actual_type =
+  user_err Pp.(str "Bad type of value for this option:" ++ spc() ++
+               str "expected " ++ str (show_value_type opt_value) ++
+               str ", got " ++ str actual_type ++ str ".")
 
 let check_int_value v = function
   | IntValue _ -> IntValue v
-  | _ -> bad_type_error ()
+  | optv -> bad_type_error optv "int"
 
 let check_bool_value v = function
   | BoolValue _ -> BoolValue v
-  | _ -> bad_type_error ()
+  | optv -> bad_type_error optv "bool"
 
 let check_string_value v = function
   | StringValue _ -> StringValue v
   | StringOptValue _ -> StringOptValue (Some v)
-  | _ -> bad_type_error ()
+  | optv -> bad_type_error optv "string"
 
 let check_unset_value v = function
   | BoolValue _ -> BoolValue false
   | IntValue _ -> IntValue None
   | StringOptValue _ -> StringOptValue None
-  | _ -> bad_type_error ()
+  | optv -> bad_type_error optv "nothing"
 
 (* Nota: For compatibility reasons, some errors are treated as
    warning. This allows a script to refer to an option that doesn't
diff --git a/library/goptions.mli b/library/goptions.mli
index 6c14d19e..3d7df18f 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -89,7 +89,7 @@ module MakeRefTable :
     (A : sig
            type t
            val compare : t -> t -> int
-           val encode : reference -> t
+           val encode : qualid -> t
 	   val subst : substitution -> t -> t
            val printer : t -> Pp.t
            val key : option_name
@@ -147,9 +147,9 @@ val get_string_table :
 
 val get_ref_table :
   option_name ->
-    < add : reference -> unit;
-      remove : reference -> unit;
-      mem : reference -> unit;
+    < add : qualid -> unit;
+      remove : qualid -> unit;
+      mem : qualid -> unit;
       print : unit >
 
 (** The first argument is a locality flag. *)
diff --git a/library/heads.ml b/library/heads.ml
deleted file mode 100644
index 198672a0..00000000
--- a/library/heads.ml
+++ /dev/null
@@ -1,193 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Names
-open Constr
-open Vars
-open Mod_subst
-open Environ
-open Globnames
-open Libobject
-open Lib
-open Context.Named.Declaration
-
-(** Characterization of the head of a term *)
-
-(* We only compute an approximation to ensure the computation is not
-   arbitrary long (e.g. the head constant of [h] defined to be
-   [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch
-   the evaluation of [phi(0)] and the head of [h] is declared unknown). *)
-
-type rigid_head_kind =
-| RigidParameter of Constant.t (* a Const without body *)
-| RigidVar of variable (* a Var without body *)
-| RigidType (* an inductive, a product or a sort *)
-
-type head_approximation =
-| RigidHead of rigid_head_kind
-| ConstructorHead
-| FlexibleHead of int * int * int * bool (* [true] if a surrounding case *)
-| NotImmediatelyComputableHead
-
-(** Registration as global tables and rollback. *)
-
-module Evalreford = struct
-  type t = evaluable_global_reference
-  let compare gr1 gr2 = match gr1, gr2 with
-  | EvalVarRef id1, EvalVarRef id2 -> Id.compare id1 id2
-  | EvalVarRef _, EvalConstRef _ -> -1
-  | EvalConstRef c1, EvalConstRef c2 ->
-    Constant.CanOrd.compare c1 c2
-  | EvalConstRef _, EvalVarRef _ -> 1
-end
-
-module Evalrefmap =
-  Map.Make (Evalreford)
-
-
-let head_map = Summary.ref Evalrefmap.empty ~name:"Head_decl"
-
-let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
-let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
-
-let kind_of_head env t =
-  let rec aux k l t b = match kind (Reduction.whd_betaiotazeta env t) with
-  | Rel n when n > k -> NotImmediatelyComputableHead
-  | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
-  | Var id ->
-      (try on_subterm k l b (variable_head id)
-       with Not_found ->
-        (* a goal variable *)
-        match lookup_named id env with
-        | LocalDef (_,c,_) -> aux k l c b
-        | LocalAssum _ -> NotImmediatelyComputableHead)
-  | Const (cst,_) ->
-      (try on_subterm k l b (constant_head cst)
-       with Not_found ->
-         CErrors.anomaly
-           Pp.(str "constant not found in kind_of_head: " ++
-               Names.Constant.print cst ++
-               str "."))
-  | Construct _ | CoFix _ ->
-      if b then NotImmediatelyComputableHead else ConstructorHead
-  | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
-  | Cast (c,_,_) -> aux k l c b
-  | Lambda (_,_,c) ->
-    begin match l with
-    | [] ->
-      let () = assert (not b) in
-      aux (k + 1) [] c b
-    | h :: l -> aux k l (subst1 h c) b
-    end
-  | LetIn _ -> assert false
-  | Meta _ | Evar _ -> NotImmediatelyComputableHead
-  | App (c,al) -> aux k (Array.to_list al @ l) c b
-  | Proj (p,c) ->
-      (try on_subterm k (c :: l) b (constant_head (Projection.constant p))
-       with Not_found -> assert false)
-
-  | Case (_,_,c,_) -> aux k [] c true
-  | Fix ((i,j),_) ->
-      let n = i.(j) in
-      try aux k [] (List.nth l n) true
-      with Failure _ -> FlexibleHead (k + n + 1, k + n + 1, 0, true)
-  and on_subterm k l with_case = function
-  | FlexibleHead (n,i,q,with_subcase) ->
-      let m = List.length l in
-      let k',rest,a =
-        if n > m then
-          (* eta-expansion *)
-          let a =
-            if i <= m then
-              (* we pick the head in the existing arguments *)
-              lift (n-m) (List.nth l (i-1))
-            else
-              (* we pick the head in the added arguments *)
-              mkRel (n-i+1) in
-          k+n-m,[],a
-        else
-          (* enough arguments to [cst] *)
-          k,List.skipn n l,List.nth l (i-1) in
-      let l' = List.make q (mkMeta 0) @ rest in
-      aux k' l' a (with_subcase || with_case)
-  | ConstructorHead when with_case -> NotImmediatelyComputableHead
-  | x -> x
-  in aux 0 [] t false
-
-(* FIXME: maybe change interface here *)
-let compute_head = function
-| EvalConstRef cst ->
-   let env = Global.env() in
-   let cb = Environ.lookup_constant cst env in
-   let is_Def = function Declarations.Def _ -> true | _ -> false in
-   let body = 
-     if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
-     then Global.body_of_constant cst else None
-   in
-     (match body with
-     | None -> RigidHead (RigidParameter cst)
-     | Some (c, _) -> kind_of_head env c)
-| EvalVarRef id ->
-    (match Global.lookup_named id with
-     | LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
-           kind_of_head (Global.env()) c
-     | _ ->
-           RigidHead (RigidVar id))
-
-let is_rigid env t =
-  match kind_of_head env t with
-  | RigidHead _ | ConstructorHead -> true
-  | _ -> false
-
-(** Registration of heads as an object *)
-
-let load_head _ (_,(ref,(k:head_approximation))) =
-  head_map := Evalrefmap.add ref k !head_map
-
-let cache_head o =
-  load_head 1 o
-
-let subst_head_approximation subst = function
-  | RigidHead (RigidParameter cst) as k ->
-      let cst,c = subst_con_kn subst cst in
-      if isConst c && Constant.equal (fst (destConst c)) cst then
-        (* A change of the prefix of the constant *)
-        k
-      else
-        (* A substitution of the constant by a functor argument *)
-        kind_of_head (Global.env()) c
-  | x -> x
-
-let subst_head (subst,(ref,k)) =
-  (subst_evaluable_reference subst ref, subst_head_approximation subst k)
-
-let discharge_head (_,(ref,k)) =
-  match ref with
-  | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
-  | EvalVarRef id -> None
-
-let rebuild_head (ref,k) =
-  (ref, compute_head ref)
-
-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;
-    subst_function = subst_head;
-    classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_head;
-    rebuild_function = rebuild_head }
-
-let declare_head c =
-  let hd = compute_head c in
-  add_anonymous_leaf (inHead (c,hd))
diff --git a/library/heads.mli b/library/heads.mli
deleted file mode 100644
index 42124299..00000000
--- a/library/heads.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Constr
-open Environ
-
-(** This module is about the computation of an approximation of the
-    head symbol of defined constants and local definitions; it
-    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
-   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
-    with a rigid head symbol *)
-
-val is_rigid : env -> constr -> bool
diff --git a/library/keys.ml b/library/keys.ml
index 34a6adab..3cadcb64 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -10,12 +10,13 @@
 
 (** Keys for unification and indexing *)
 
-open Globnames
-open Term
+open Names
+open Constr
 open Libobject
+open Globnames
 
 type key =
-  | KGlob of global_reference
+  | KGlob of GlobRef.t
   | KLam
   | KLet
   | KProd
@@ -126,7 +127,7 @@ let constr_key kind c =
       | Construct (c,u) -> KGlob (ConstructRef c)
       | Var id -> KGlob (VarRef id)
       | App (f, _) -> aux f
-      | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p))
+      | Proj (p, _) -> KGlob (ConstRef (Projection.constant p))
       | Cast (p, _, _) -> aux p
       | Lambda _ -> KLam 
       | Prod _ -> KProd
diff --git a/library/keys.mli b/library/keys.mli
index 1fb9a3de..19838365 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Globnames
-
 type key
 
 val declare_equiv_keys : key -> key -> unit
@@ -21,5 +19,5 @@ val equiv_keys : key -> key -> bool
 val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
 (** Compute the head key of a term. *)
 
-val pr_keys : (global_reference -> Pp.t) -> Pp.t
+val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t
 (** Pretty-print the mapping *)
diff --git a/library/lib.ml b/library/lib.ml
index 543cb45b..8ebe4489 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -26,13 +26,11 @@ type node =
   | Leaf of obj
   | CompilingLibrary of object_prefix
   | OpenedModule of is_type * export * object_prefix * Summary.frozen
-  | ClosedModule  of library_segment
   | OpenedSection of object_prefix * Summary.frozen
-  | ClosedSection of library_segment
 
-and library_entry = object_name * node
+type library_entry = object_name * node
 
-and library_segment = library_entry list
+type library_segment = library_entry list
 
 type lib_objects =  (Names.Id.t * obj) list
 
@@ -51,7 +49,7 @@ let subst_objects subst seg =
       if obj' == obj then node else
 	(id, obj')
   in
-    List.smartmap subst_one seg
+    List.Smart.map subst_one seg
 
 (*let load_and_subst_objects i prefix subst seg =
   List.rev (List.fold_left (fun seg (id,obj as node) ->
@@ -73,10 +71,6 @@ let classify_segment seg =
 		 clean ((id,o')::substl, keepl, anticipl) stk
 	     | Anticipate o' ->
 		 clean (substl, keepl, o'::anticipl) stk)
-    | (_,ClosedSection _) :: stk -> clean acc stk
-    (* 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
     | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
       user_err ~hdr:"Lib.classify_segment"
@@ -183,22 +177,11 @@ let split_lib_gen test =
     | before -> after,equal,before
   in
   let rec findeq after = function
-    | hd :: before ->
-      	if test hd
-	then Some (collect after [hd] before)
-	else (match hd with
-		| (sp,ClosedModule  seg)
-		| (sp,ClosedSection seg) ->
-		    (match findeq after seg with
-		       | None -> findeq (hd::after) before
-		       | Some (sub_after,sub_equal,sub_before) ->
-			   Some (sub_after, sub_equal, (List.append sub_before before)))
-		| _ -> findeq (hd::after) before)
-    | [] -> None
+    | hd :: before when test hd -> collect after [hd] before
+    | hd :: before -> findeq (hd::after) before
+    | [] -> user_err Pp.(str "no such entry")
   in
-    match findeq [] !lib_state.lib_stk with
-      | None -> user_err Pp.(str "no such entry")
-      | Some r -> r
+  findeq [] !lib_state.lib_stk
 
 let eq_object_name (fp1, kn1) (fp2, kn2) =
   eq_full_path fp1 fp2 && Names.KerName.equal kn1 kn2
@@ -318,7 +301,6 @@ let end_mod is_type =
   in
   let (after,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
-  add_entry oname (ClosedModule (List.rev (mark::after)));
   let prefix = !lib_state.path_prefix in
   recalc_path_prefix ();
   (oname, prefix, fs, after)
@@ -416,7 +398,7 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
+type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
 
 type variable_context = variable_info list
 type abstr_info = {
@@ -566,7 +548,6 @@ let discharge_item ((sp,_ as oname),e) =
   match e with
   | Leaf lobj ->
       Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
-  | ClosedSection _ | ClosedModule _ -> None
   | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly (Pp.str "discharge_item.")
 
@@ -580,13 +561,10 @@ let close_section () =
   in
   let (secdecls,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
-  let full_olddir = !lib_state.path_prefix.obj_dir in
   pop_path_prefix ();
-  add_entry oname (ClosedSection (List.rev (mark::secdecls)));
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
-  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
-  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
 
 (* State and initialization. *)
 
@@ -602,10 +580,8 @@ let freeze ~marshallable =
         | n, (CompilingLibrary _ as x) -> Some (n,x)
         | n, OpenedModule (it,e,op,_) ->
                Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
-        | n, ClosedModule _ -> Some (n,ClosedModule [])
         | n, OpenedSection (op, _) ->
-               Some(n,OpenedSection(op,Summary.empty_frozen))
-        | n, ClosedSection _ -> Some (n,ClosedSection []))
+               Some(n,OpenedSection(op,Summary.empty_frozen)))
       !lib_state.lib_stk in
     { !lib_state with lib_stk }
   | _ ->
@@ -669,6 +645,14 @@ let discharge_kn kn =
 let discharge_con cst =
   if con_defined_in_sec cst then Globnames.pop_con cst else cst
 
+let discharge_proj_repr =
+  Projection.Repr.map_npars (fun mind npars ->
+      if not (defined_in_sec mind) then mind, npars
+      else
+        let modlist = replacement_context () in
+        let _, newpars = Mindmap.find mind (snd modlist) in
+        Globnames.pop_kn mind, npars + Array.length newpars)
+
 let discharge_inductive (kn,i) =
   (discharge_kn kn,i)
 
diff --git a/library/lib.mli b/library/lib.mli
index 26f1718c..9933b762 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 
 (** Lib: record of operations, backtrack, low-level sections *)
 
@@ -22,13 +23,11 @@ type node =
   | Leaf of Libobject.obj
   | CompilingLibrary of Libnames.object_prefix
   | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen
-  | ClosedModule  of library_segment
   | OpenedSection of Libnames.object_prefix * Summary.frozen
-  | ClosedSection of library_segment
 
-and library_segment = (Libnames.object_name * node) list
+type library_segment = (Libnames.object_name * node) list
 
-type lib_objects = (Names.Id.t * Libobject.obj) list
+type lib_objects = (Id.t * Libobject.obj) list
 
 (** {6 Object iteration functions. } *)
 
@@ -54,13 +53,13 @@ val segment_of_objects :
 (** Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
-val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
+val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name
 val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
 val pull_to_head : Libnames.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
-val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name
+val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name
 
 (** {6 ... } *)
 
@@ -76,15 +75,15 @@ val contents_after : Libnames.object_name -> library_segment
 (** {6 Functions relative to current path } *)
 
 (** User-side names *)
-val cwd : unit -> Names.DirPath.t
-val cwd_except_section : unit -> Names.DirPath.t
-val current_dirpath : bool -> Names.DirPath.t (* false = except sections *)
-val make_path : Names.Id.t -> Libnames.full_path
-val make_path_except_section : Names.Id.t -> Libnames.full_path
+val cwd : unit -> DirPath.t
+val cwd_except_section : unit -> DirPath.t
+val current_dirpath : bool -> DirPath.t (* false = except sections *)
+val make_path : Id.t -> Libnames.full_path
+val make_path_except_section : Id.t -> Libnames.full_path
 
 (** Kernel-side names *)
-val current_mp : unit -> Names.ModPath.t
-val make_kn : Names.Id.t -> Names.KerName.t
+val current_mp : unit -> ModPath.t
+val make_kn : Id.t -> KerName.t
 
 (** Are we inside an opened section *)
 val sections_are_opened : unit -> bool
@@ -97,19 +96,19 @@ val is_modtype : unit -> bool
    if the latest module started is a module type.  *)
 val is_modtype_strict : unit -> bool
 val is_module : unit -> bool
-val current_mod_id : unit -> Names.module_ident
+val current_mod_id : unit -> module_ident
 
 (** Returns the opening node of a given name *)
-val find_opening_node : Names.Id.t -> node
+val find_opening_node : Id.t -> node
 
 (** {6 Modules and module types } *)
 
 val start_module :
-  export -> Names.module_ident -> Names.ModPath.t ->
+  export -> module_ident -> ModPath.t ->
   Summary.frozen -> Libnames.object_prefix
 
 val start_modtype :
-  Names.module_ident -> Names.ModPath.t ->
+  module_ident -> ModPath.t ->
   Summary.frozen -> Libnames.object_prefix
 
 val end_module :
@@ -124,23 +123,23 @@ val end_modtype :
 
 (** {6 Compilation units } *)
 
-val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
-val end_compilation_checks : Names.DirPath.t -> Libnames.object_name
+val start_compilation : DirPath.t -> ModPath.t -> unit
+val end_compilation_checks : DirPath.t -> Libnames.object_name
 val end_compilation :
   Libnames.object_name-> Libnames.object_prefix * library_segment
 
 (** The function [library_dp] returns the [DirPath.t] of the current
    compiling library (or [default_library]) *)
-val library_dp : unit -> Names.DirPath.t
+val library_dp : unit -> DirPath.t
 
 (** Extract the library part of a name even if in a section *)
-val dp_of_mp : Names.ModPath.t -> Names.DirPath.t
-val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list
-val library_part :  Globnames.global_reference -> Names.DirPath.t
+val dp_of_mp : ModPath.t -> DirPath.t
+val split_modpath : ModPath.t -> DirPath.t * Id.t list
+val library_part :  GlobRef.t -> DirPath.t
 
 (** {6 Sections } *)
 
-val open_section : Names.Id.t -> unit
+val open_section : Id.t -> unit
 val close_section : unit -> unit
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
@@ -153,7 +152,7 @@ val unfreeze : frozen -> unit
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
-type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
+type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
 type variable_context = variable_info list 
 type abstr_info = private {
   abstr_ctx : variable_context;
@@ -164,31 +163,32 @@ type abstr_info = private {
   (** Universe quantification, same length as the substitution *)
 }
 
-val instance_from_variable_context : variable_context -> Names.Id.t array
-val named_of_variable_context : variable_context -> Context.Named.t
+val instance_from_variable_context : variable_context -> Id.t array
+val named_of_variable_context : variable_context -> Constr.named_context
 
-val section_segment_of_constant : Names.Constant.t -> abstr_info
-val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info
-val section_segment_of_reference : Globnames.global_reference -> abstr_info
+val section_segment_of_constant : Constant.t -> abstr_info
+val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
+val section_segment_of_reference : GlobRef.t -> abstr_info
 
-val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
+val variable_section_segment_of_reference : GlobRef.t -> variable_context
 
-val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array
-val is_in_section : Globnames.global_reference -> bool
+val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
+val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
+val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
 val add_section_context : Univ.ContextSet.t -> unit
 val add_section_constant : Decl_kinds.polymorphic ->
-  Names.Constant.t -> Context.Named.t -> unit
+  Constant.t -> Constr.named_context -> unit
 val add_section_kn : Decl_kinds.polymorphic ->
-  Names.MutInd.t -> Context.Named.t -> unit
+  MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)
 
-val discharge_kn :  Names.MutInd.t -> Names.MutInd.t
-val discharge_con : Names.Constant.t -> Names.Constant.t
-val discharge_global : Globnames.global_reference -> Globnames.global_reference
-val discharge_inductive : Names.inductive -> Names.inductive
+val discharge_kn :  MutInd.t -> MutInd.t
+val discharge_con : Constant.t -> Constant.t
+val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t
+val discharge_global : GlobRef.t -> GlobRef.t
+val discharge_inductive : inductive -> inductive
 val discharge_abstract_universe_context :
   abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t
diff --git a/library/libnames.ml b/library/libnames.ml
index d8473132..23085048 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -15,8 +15,6 @@ open Names
 
 (**********************************************)
 
-let pr_dirpath sl = DirPath.print sl
-
 (*s Operations on dirpaths *)
 
 let split_dirpath d = match DirPath.repr d with
@@ -80,8 +78,6 @@ let dirpath_of_string s =
   in
   DirPath.make path
 
-let string_of_dirpath = Names.DirPath.to_string
-
 module Dirset = Set.Make(DirPath)
 module Dirmap = Map.Make(DirPath)
 
@@ -138,23 +134,33 @@ let restrict_path n sp =
   make_path (DirPath.make dir') s
 
 (*s qualified names *)
-type qualid = full_path
+type qualid_r = full_path
+type qualid = qualid_r CAst.t
 
-let make_qualid = make_path
-let repr_qualid = repr_path
+let make_qualid ?loc pa id = CAst.make ?loc (make_path pa id)
+let repr_qualid {CAst.v=qid} = repr_path qid
 
-let qualid_eq = eq_full_path
+let qualid_eq qid1 qid2 = eq_full_path qid1.CAst.v qid2.CAst.v
 
-let string_of_qualid = string_of_path
-let pr_qualid = pr_path
+let string_of_qualid qid = string_of_path qid.CAst.v
+let pr_qualid qid = pr_path qid.CAst.v
 
-let qualid_of_string = path_of_string
+let qualid_of_string ?loc s = CAst.make ?loc @@ path_of_string s
 
-let qualid_of_path sp = sp
-let qualid_of_ident id = make_qualid DirPath.empty id
-let qualid_of_dirpath dir =
+let qualid_of_path ?loc sp = CAst.make ?loc sp
+let qualid_of_ident ?loc id = make_qualid ?loc DirPath.empty id
+let qualid_of_dirpath ?loc dir =
   let (l,a) = split_dirpath dir in
-  make_qualid l a
+  make_qualid ?loc l a
+
+let qualid_is_ident qid =
+  DirPath.is_empty qid.CAst.v.dirpath
+
+let qualid_basename qid =
+  qid.CAst.v.basename
+
+let qualid_path qid =
+  qid.CAst.v.dirpath
 
 type object_name = full_path * KerName.t
 
@@ -174,8 +180,6 @@ type global_dir_reference =
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of DirPath.t
-      (* this won't last long I hope! *)
 
 let eq_op op1 op2 =
   DirPath.equal op1.obj_dir op2.obj_dir &&
@@ -187,55 +191,8 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
 | DirModule op1, DirModule op2 -> eq_op op1 op2
-| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2
-| _ -> false
-
-type reference_r =
-  | Qualid of qualid
-  | Ident of Id.t
-type reference = reference_r CAst.t
-
-let qualid_of_reference = CAst.map (function
-  | Qualid qid -> qid
-  | Ident id -> qualid_of_ident id)
-
-let string_of_reference = CAst.with_val (function
-  | Qualid qid -> string_of_qualid qid
-  | Ident id -> Id.to_string id)
-
-let pr_reference = CAst.with_val (function
-  | Qualid qid -> pr_qualid qid
-  | Ident id -> Id.print id)
-
-let eq_reference {CAst.v=r1} {CAst.v=r2} = match r1, r2 with
-| Qualid q1, Qualid q2 -> qualid_eq q1 q2
-| Ident id1, Ident id2 -> Id.equal id1 id2
 | _ -> false
 
-let join_reference {CAst.loc=l1;v=ns} {CAst.loc=l2;v=r} =
-  CAst.make ?loc:(Loc.merge_opt l1 l2) (
-  match ns , r with
-    Qualid q1, Qualid q2 ->
-      let (dp1,id1) = repr_qualid q1 in
-      let (dp2,id2) = repr_qualid q2 in
-      Qualid (make_qualid
-		(append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2)
-		id2)
-  | Qualid q1, Ident id2 ->
-    let (dp1,id1) = repr_qualid q1 in
-    Qualid (make_qualid
-	      (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1)))
-	      id2)
-  | Ident id1, Qualid q2 ->
-    let (dp2,id2) = repr_qualid q2 in
-    Qualid (make_qualid
-      (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2)
-      id2)
-  | Ident id1, Ident id2 ->
-    Qualid (make_qualid
-      (dirpath_of_string (Names.Id.to_string id1)) id2)
-  )
-
 (* Default paths *)
 let default_library = Names.DirPath.initial (* = ["Top"] *)
 
@@ -243,8 +200,3 @@ let default_library = Names.DirPath.initial (* = ["Top"] *)
 let coq_string = "Coq"
 let coq_root = Id.of_string coq_string
 let default_root_prefix = DirPath.empty
-
-(* Deprecated synonyms *)
-
-let make_short_qualid = qualid_of_ident
-let qualid_of_sp = qualid_of_path
diff --git a/library/libnames.mli b/library/libnames.mli
index 9dad2612..447eecbb 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -14,12 +14,6 @@ open Names
 (** {6 Dirpaths } *)
 val dirpath_of_string : string -> DirPath.t
 
-val pr_dirpath : DirPath.t -> Pp.t
-[@@ocaml.deprecated "Alias for DirPath.print"]
-
-val string_of_dirpath : DirPath.t -> string
-[@@ocaml.deprecated "Alias for DirPath.to_string"]
-
 (** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *)
 val pop_dirpath : DirPath.t -> DirPath.t
 
@@ -71,23 +65,28 @@ val restrict_path : int -> full_path -> full_path
     qualifications of absolute names, including single identifiers.
     The [qualid] are used to access the name table. *)
 
-type qualid
+type qualid_r
+type qualid = qualid_r CAst.t
 
-val make_qualid : DirPath.t -> Id.t -> qualid
+val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid
 val repr_qualid : qualid -> DirPath.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
 val pr_qualid : qualid -> Pp.t
 val string_of_qualid : qualid -> string
-val qualid_of_string : string -> qualid
+val qualid_of_string : ?loc:Loc.t -> string -> qualid
 
 (** Turns an absolute name, a dirpath, or an Id.t into a
    qualified name denoting the same name *)
 
-val qualid_of_path : full_path -> qualid
-val qualid_of_dirpath : DirPath.t -> qualid
-val qualid_of_ident : Id.t -> qualid
+val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
+val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
+val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+
+val qualid_is_ident : qualid -> bool
+val qualid_path : qualid -> DirPath.t
+val qualid_basename : qualid -> Id.t
 
 (** Both names are passed to objects: a "semantic" [kernel_name], which
    can be substituted and a "syntactic" [full_path] which can be printed
@@ -125,27 +124,11 @@ type global_dir_reference =
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of DirPath.t
-      (** this won't last long I hope! *)
 
 val eq_global_dir_reference : 
   global_dir_reference -> global_dir_reference -> bool
 
 (** {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 *)
-
-type reference_r =
-  | Qualid of qualid
-  | Ident of Id.t
-type reference = reference_r CAst.t
-
-val eq_reference : reference -> reference -> bool
-val qualid_of_reference : reference -> qualid CAst.t
-val string_of_reference : reference -> string
-val pr_reference : reference -> Pp.t
-val join_reference : reference -> reference -> reference
 
 (** some preset paths *)
 val default_library : DirPath.t
@@ -157,10 +140,3 @@ val coq_string : string (** "Coq" *)
 (** This is the default root prefix for developments which doesn't
    mention a root *)
 val default_root_prefix : DirPath.t
-
-(** Deprecated synonyms *)
-val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *)
-[@@ocaml.deprecated "Alias for qualid_of_ident"]
-
-val qualid_of_sp : full_path -> qualid (** = qualid_of_path *)
-[@@ocaml.deprecated "Alias for qualid_of_sp"]
diff --git a/library/libobject.ml b/library/libobject.ml
index c5cd0152..79a3fed1 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -98,7 +98,7 @@ let declare_object_full odecl = declare_object_full odecl
 (* this function describes how the cache, load, open, and export functions
    are triggered. *)
 
-let apply_dyn_fun deflt f lobj =
+let apply_dyn_fun f lobj =
   let tag = object_tag lobj in
   let dodecl =
     try Hashtbl.find cache_tab tag
@@ -107,24 +107,24 @@ let apply_dyn_fun deflt f lobj =
   f dodecl
 
 let cache_object ((_,lobj) as node) =
-  apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
+  apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
 
 let load_object i ((_,lobj) as node) =
-  apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj
+  apply_dyn_fun (fun d -> d.dyn_load_function i node) lobj
 
 let open_object i ((_,lobj) as node) =
-  apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj
+  apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj
 
 let subst_object ((_,lobj) as node) = 
-  apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
+  apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj
 
 let classify_object lobj =
-  apply_dyn_fun Dispose (fun d -> d.dyn_classify_function lobj) lobj
+  apply_dyn_fun (fun d -> d.dyn_classify_function lobj) lobj
 
 let discharge_object ((_,lobj) as node) =
-  apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
+  apply_dyn_fun (fun d -> d.dyn_discharge_function node) lobj
 
 let rebuild_object lobj =
-  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
+  apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj
 
 let dump = Dyn.dump
diff --git a/library/library.ml b/library/library.ml
index 56d2709d..0ff82d7c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -167,7 +167,7 @@ let opened_libraries () = !libraries_imports_list
 
 let register_loaded_library m =
   let libname = m.libsum_name in
-  let link m =
+  let link () =
     let dirname = Filename.dirname (library_full_filename libname) in
     let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
@@ -176,7 +176,7 @@ let register_loaded_library m =
       Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
-    | [] -> link m; [libname]
+    | [] -> link (); [libname]
     | m'::_ as l when DirPath.equal m' libname -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
@@ -288,16 +288,15 @@ let locate_absolute_library dir =
     try
       let name = Id.to_string base ^ ext in
       let _, file = System.where_in_path ~warn:false loadpath name in
-      [file]
-    with Not_found -> [] in
-  match find ".vo" @ find ".vio" with
-  | [] -> raise LibNotFound
-  | [file] -> file
-  | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
+      Some file
+    with Not_found -> None in
+  match find ".vo", find ".vio" with
+  | None, None -> raise LibNotFound
+  | Some file, None | None, Some file -> file
+  | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
     warn_several_object_files (vi, vo);
     vi
-  | [vo;vi] -> vo
-  | _ -> assert false
+  | Some vo, Some _ -> vo
 
 let locate_qualified_library ?root ?(warn = true) qid =
   (* Search library in loadpath *)
@@ -309,18 +308,17 @@ let locate_qualified_library ?root ?(warn = true) qid =
       let name = Id.to_string base ^ ext in
       let lpath, file =
         System.where_in_path ~warn (List.map fst loadpath) name in
-      [lpath, file]
-    with Not_found -> [] in
+      Some (lpath, file)
+    with Not_found -> None in
   let lpath, file =
-    match find ".vo" @ find ".vio" with
-    | [] -> raise LibNotFound
-    | [lpath, file] -> lpath, file
-    | [lpath_vo, vo; lpath_vi, vi]
+    match find ".vo", find ".vio" with
+    | None, None -> raise LibNotFound
+    | Some res, None | None, Some res -> res
+    | Some (_, vo), Some (_, vi as resvi)
       when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
       warn_several_object_files (vi, vo);
-       lpath_vi, vi
-    | [lpath_vo, vo; _ ] -> lpath_vo, vo
-    | _ -> assert false
+       resvi
+    | Some resvo, Some _ -> resvo
   in
   let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in
   (* Look if loaded *)
@@ -577,10 +575,10 @@ let require_library_from_dirpath modrefl export =
 
 (* the function called by Vernacentries.vernac_import *)
 
-let safe_locate_module {CAst.loc;v=qid} =
+let safe_locate_module qid =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err ?loc ~hdr:"import_library"
+    user_err ?loc:qid.CAst.loc ~hdr:"import_library"
       (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
@@ -595,18 +593,18 @@ let import_module export modl =
     | [] -> ()
     | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
   let rec aux acc = function
-    | ({CAst.loc; v=dir} as m) :: l ->
+    | qid :: l ->
         let m,acc =
-          try Nametab.locate_module dir, acc
-          with Not_found-> flush acc; safe_locate_module m, [] in
+          try Nametab.locate_module qid, acc
+          with Not_found-> flush acc; safe_locate_module qid, [] in
         (match m with
         | MPfile dir -> aux (dir::acc) l
         | mp ->
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err ?loc ~hdr:"import_library"
-                (pr_qualid dir ++ str " is not a module"))
+              user_err ?loc:qid.CAst.loc ~hdr:"import_library"
+                (pr_qualid qid ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
diff --git a/library/library.mli b/library/library.mli
index 0877ebb5..d5815afc 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -36,7 +36,7 @@ type seg_proofs = Constr.constr Future.computation array
 
 (** 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 CAst.t list -> unit
+val import_module : bool -> qualid list -> unit
 
 (** Start the compilation of a file as a library. The first argument must be
     output file, and the 
diff --git a/library/library.mllib b/library/library.mllib
index e43bfb5a..9cacaba4 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -4,6 +4,7 @@ Libobject
 Summary
 Nametab
 Global
+Decl_kinds
 Lib
 Declaremods
 Loadpath
@@ -13,6 +14,5 @@ Kindops
 Dischargedhypsmap
 Goptions
 Decls
-Heads
 Keys
 Coqlib
diff --git a/library/nametab.ml b/library/nametab.ml
index 2046bf75..a3b3ca6e 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,8 +18,8 @@ open Globnames
 
 exception GlobalizationError of qualid
 
-let error_global_not_found {CAst.loc;v} =
-  Loc.raise ?loc (GlobalizationError v)
+let error_global_not_found qid =
+  Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid)
 
 (* The visibility can be registered either
    - for all suffixes not shorter then a given int - when the object
@@ -69,7 +69,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
-  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 end
 
@@ -220,7 +220,7 @@ let exists uname tab =
   with
       Not_found -> false
 
-let shortest_qualid ctx uname tab =
+let shortest_qualid ?loc ctx uname tab =
   let id,dir = U.repr uname in
   let hidden = Id.Set.mem id ctx in
   let rec find_uname pos dir tree =
@@ -235,7 +235,7 @@ let shortest_qualid ctx uname tab =
   in
   let ptab = Id.Map.find id tab in
   let found_dir = find_uname [] dir ptab in
-    make_qualid (DirPath.make found_dir) id
+    make_qualid ?loc (DirPath.make found_dir) id
 
 let push_node node l =
   match node with
@@ -432,7 +432,6 @@ let full_name_module qid =
 let locate_section qid =
   match locate_dir qid with
     | DirOpenSection { obj_dir; _ } -> obj_dir
-    | DirClosedSection dir -> dir
     | _ -> raise Not_found
 
 let locate_all qid =
@@ -459,14 +458,13 @@ let global_of_path sp =
 
 let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab
 
-let global ({CAst.loc;v=r} as lr)=
-  let {CAst.loc; v} as qid = qualid_of_reference lr in
-  try match locate_extended v with
+let global qid =
+  try match locate_extended qid with
     | TrueGlobal ref -> ref
     | SynDef _ ->
-        user_err ?loc ~hdr:"global"
+        user_err ?loc:qid.CAst.loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
-           pr_qualid v)
+           pr_qualid qid)
   with Not_found ->
     error_global_not_found qid
 
@@ -511,40 +509,40 @@ let path_of_universe mp =
 
 (* Shortest qualid functions **********************************************)
 
-let shortest_qualid_of_global ctx ref =
+let shortest_qualid_of_global ?loc ctx ref =
   match ref with
-    | VarRef id -> make_qualid DirPath.empty id
+    | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
-        ExtRefTab.shortest_qualid ctx sp !the_ccitab
+        ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
-let shortest_qualid_of_syndef ctx kn =
+let shortest_qualid_of_syndef ?loc ctx kn =
   let sp = path_of_syndef kn in
-    ExtRefTab.shortest_qualid ctx sp !the_ccitab
+    ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
-let shortest_qualid_of_module mp =
+let shortest_qualid_of_module ?loc mp =
   let dir = MPmap.find mp !the_modrevtab in
-    DirTab.shortest_qualid Id.Set.empty dir !the_dirtab
+    DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab
 
-let shortest_qualid_of_modtype kn =
+let shortest_qualid_of_modtype ?loc kn =
   let sp = MPmap.find kn !the_modtyperevtab in
-    MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab
+    MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab
 
-let shortest_qualid_of_universe kn =
+let shortest_qualid_of_universe ?loc kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
-    UnivTab.shortest_qualid Id.Set.empty sp !the_univtab
+    UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as e ->
     if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
 
-let global_inductive ({CAst.loc; v=r} as lr) =
-  match global lr with
+let global_inductive qid =
+  match global qid with
   | IndRef ind -> ind
   | ref ->
-      user_err ?loc ~hdr:"global_inductive"
-        (pr_reference lr ++ spc () ++ str "is not an inductive type")
+      user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+        (pr_qualid qid ++ spc () ++ str "is not an inductive type")
 
 (********************************************************************)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index cd28518a..57e9141d 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -61,7 +61,7 @@ open Globnames
 exception GlobalizationError of qualid
 
 (** Raises a globalization error *)
-val error_global_not_found : qualid CAst.t -> 'a
+val error_global_not_found : qualid -> 'a
 
 (** {6 Register visibility of things } *)
 
@@ -75,7 +75,7 @@ val error_global_not_found : qualid CAst.t -> 'a
 
 type visibility = Until of int | Exactly of int
 
-val push : visibility -> full_path -> global_reference -> unit
+val push : visibility -> full_path -> GlobRef.t -> unit
 val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
@@ -91,7 +91,7 @@ val push_universe : visibility -> full_path -> universe_id -> unit
 (** These functions globalize a (partially) qualified name or fail with
    [Not_found] *)
 
-val locate : qualid -> global_reference
+val locate : qualid -> GlobRef.t
 val locate_extended : qualid -> extended_global_reference
 val locate_constant : qualid -> Constant.t
 val locate_syndef : qualid -> syndef_name
@@ -105,20 +105,20 @@ val locate_universe : qualid -> universe_id
    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
+val global : qualid -> GlobRef.t
+val global_inductive : qualid -> inductive
 
 (** 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_all : qualid -> GlobRef.t list
 val locate_extended_all : qualid -> extended_global_reference list
 val locate_extended_all_dir : qualid -> global_dir_reference list
 val locate_extended_all_modtype : qualid -> ModPath.t list
 
 (** Mapping a full path to a global reference *)
 
-val global_of_path : full_path -> global_reference
+val global_of_path : full_path -> GlobRef.t
 val extended_global_of_path : full_path -> extended_global_reference
 
 (** {6 These functions tell if the given absolute name is already taken } *)
@@ -144,7 +144,7 @@ val full_name_module : qualid -> DirPath.t
    definition, and the (full) dirpath associated to a module path *)
 
 val path_of_syndef : syndef_name -> full_path
-val path_of_global : global_reference -> full_path
+val path_of_global : GlobRef.t -> full_path
 val dirpath_of_module : ModPath.t -> DirPath.t
 val path_of_modtype : ModPath.t -> full_path
 
@@ -155,12 +155,12 @@ val path_of_universe : universe_id -> full_path
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
 
-val dirpath_of_global : global_reference -> DirPath.t
-val basename_of_global : global_reference -> Id.t
+val dirpath_of_global : GlobRef.t -> DirPath.t
+val basename_of_global : GlobRef.t -> Id.t
 
 (** Printing of global references using names as short as possible.
     @raise Not_found when the reference is not in the global tables. *)
-val pr_global_env : Id.Set.t -> global_reference -> Pp.t
+val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
 
 
 (** The [shortest_qualid] functions given an object with [user_name]
@@ -168,16 +168,16 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t
    Coq.A.B.x that denotes the same object.
    @raise Not_found for unknown objects. *)
 
-val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
-val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
-val shortest_qualid_of_modtype : ModPath.t -> qualid
-val shortest_qualid_of_module : ModPath.t -> qualid
-val shortest_qualid_of_universe : universe_id -> qualid
+val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
+val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
+val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
+val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
 
 (** 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 -> GlobRef.t (** = global_of_path *)
 
 (** {5 Generic name handling} *)
 
@@ -207,7 +207,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
-  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 end
 
diff --git a/library/summary.ml b/library/summary.ml
index 7ef19fbf..9b229459 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -75,20 +75,6 @@ let freeze_summaries ~marshallable : frozen =
     ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
   }
 
-let unfreeze_single name state =
-  let decl =
-    try String.Map.find name !sum_map
-    with
-    | Not_found ->
-      CErrors.anomaly Pp.(str "trying to unfreeze unregistered summary " ++ str name)
-  in
-  try decl.unfreeze_function state
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    Feedback.msg_warning
-      Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
-    iraise e
-
 let warn_summary_out_of_scope =
   let name = "summary-out-of-scope" in
   let category = "dev" in
@@ -142,36 +128,6 @@ let remove_from_summary st tag =
   let summaries = String.Map.remove id st.summaries in
   {st with summaries}
 
-(** Selective freeze *)
-
-type frozen_bits = Dyn.t String.Map.t
-
-let freeze_summary ~marshallable ?(complement=false) ids =
-  let sub_map = String.Map.filter (fun id _ -> complement <> List.(mem id ids)) !sum_map in
-  String.Map.map (fun decl -> decl.freeze_function marshallable) sub_map
-
-let unfreeze_summary = String.Map.iter unfreeze_single
-
-let surgery_summary { summaries; ml_module } bits =
-  let summaries =
-    String.Map.fold (fun hash state sum -> String.Map.set hash state sum ) summaries bits in
-  { summaries; ml_module }
-
-let project_summary { summaries; ml_module } ?(complement=false) ids =
-  String.Map.filter (fun name _ -> complement <> List.(mem name ids)) summaries
-
-let pointer_equal l1 l2 =
-  let ptr_equal d1 d2 =
-    let Dyn.Dyn (t1, x1) = d1 in
-    let Dyn.Dyn (t2, x2) = d2 in
-    match Dyn.eq t1 t2 with
-    | None -> false
-    | Some Refl -> x1 == x2
-  in
-  let l1, l2 = String.Map.bindings l1, String.Map.bindings l2 in
-  CList.for_all2eq
-    (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
-
 (** All-in-one reference declaration + registration *)
 
 let ref_tag ?(freeze=fun _ r -> r) ~name x =
diff --git a/library/summary.mli b/library/summary.mli
index ed6c26b1..7d91a791 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -91,25 +91,5 @@ val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen
 val project_from_summary : frozen -> 'a Dyn.tag -> 'a
 val remove_from_summary : frozen -> 'a Dyn.tag -> frozen
 
-(** The type [frozen_bits] is a snapshot of some of the registered
-    tables. It is DEPRECATED in favor of the typed projection
-    version. *)
-
-type frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-
-[@@@ocaml.warning "-3"]
-val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val unfreeze_summary : frozen_bits -> unit
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val surgery_summary : frozen -> frozen_bits -> frozen
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val pointer_equal : frozen_bits -> frozen_bits -> bool
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-[@@@ocaml.warning "+3"]
-
 (** {6 Debug} *)
 val dump : unit -> (int * string) list