Swapping Context and Constr: defining declarations on constr in Constr.

This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.

Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).

47 files changed, 162 insertions, 153 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index f3fc126f92..cbb95625fc 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -53,6 +53,16 @@ Printer.ml API
   pr_subgoal and pr_goal was removed to simplify the code.  It was
   earlierly used by PCoq.
 
+Kernel
+
+  The following renamings happened:
+  - `Context.Rel.t` into `Constr.rel_context`
+  - `Context.Named.t` into `Constr.named_context`
+  - `Context.Compacted.t` into `Constr.compacted_context`
+  - `Context.Rel.Declaration.t` into `Constr.rel_declaration`
+  - `Context.Named.Declaration.t` into `Constr.named_declaration`
+  - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration`
+
 Source code organization
 
 - We have eliminated / fused some redundant modules and relocated a
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 913825a9f3..ecb36615f3 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -321,7 +321,7 @@ sig
   val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
   (** Physical identity. Does not care for defined evars. *)
 
-  val to_named_context : (t, types) Context.Named.pt -> Context.Named.t
+  val to_named_context : (t, types) Context.Named.pt -> Constr.named_context
 
   val to_sorts : ESorts.t -> Sorts.t
   (** Physical identity. Does not care for normalization. *)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 8ce1b625f2..135aa73fcd 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -128,7 +128,7 @@ val advance : evar_map -> Evar.t -> Evar.t option
     [nf_evar]. *)
 
 val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
-val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
+val undefined_evars_of_named_context : evar_map -> Constr.named_context -> Evar.Set.t
 val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 type undefined_evars_cache
@@ -161,7 +161,7 @@ val jv_nf_evar :
 val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
+val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context
 val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 64db704517..d638bb2d33 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -230,7 +230,7 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option
 
 val existential_opt_value0 : evar_map -> existential -> constr option
 
-val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
 val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
diff --git a/engine/termops.mli b/engine/termops.mli
index f9aa6ba63c..80988989f1 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -43,14 +43,14 @@ val it_mkProd : types -> (Name.t * types) list -> types
 val it_mkLambda : constr -> (Name.t * types) list -> constr
 val it_mkProd_or_LetIn : types -> rel_context -> types
 val it_mkProd_wo_LetIn : types -> rel_context -> types
-val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
+val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
 val it_mkNamedProd_or_LetIn : types -> named_context -> types
-val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types
+val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
 val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
-val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
+val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
 
 (** {6 Generic iterators on constr} *)
 
@@ -225,7 +225,7 @@ val names_of_rel_context : env -> names_context
 (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has
    [n] hypotheses, excluding local definitions, and [Γ₁], if not empty,
    starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *)
-val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
+val context_chop : int -> Constr.rel_context -> Constr.rel_context * Constr.rel_context
 
 (* [env_rel_context_chop n env] extracts out the [n] top declarations
    of the rel_context part of [env], counting both local definitions and
@@ -239,19 +239,19 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t
 (** other signature iterators *)
 val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list
-val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
-val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t
-val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
+val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
+val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
+val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *)
 
 val map_rel_context_in_env :
-  (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t
+  (env -> Constr.constr -> Constr.constr) -> env -> Constr.rel_context -> Constr.rel_context
 val map_rel_context_with_binders :
   (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
 val fold_named_context_both_sides :
-  ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
-    Context.Named.t -> init:'a -> 'a
+  ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) ->
+    Constr.named_context -> init:'a -> 'a
 val mem_named_context_val : Id.t -> named_context_val -> bool
-val compact_named_context : Context.Named.t -> Context.Compacted.t
+val compact_named_context : Constr.named_context -> Constr.compacted_context
 
 val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
 val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
@@ -313,6 +313,6 @@ val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
 val print_constr     : constr -> Pp.t
 val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
 val print_named_context : env -> Pp.t
-val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t
+val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
 val print_rel_context : env -> Pp.t
 val print_env : env -> Pp.t
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 83ad9af338..288a0bfe00 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -22,7 +22,7 @@ open Libobject
 open Nameops
 open Context.Rel.Declaration
 
-exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *)
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
 let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m))
 
 module RelDecl = Context.Rel.Declaration
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index a8492095ec..437fef1753 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -38,14 +38,14 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
+  Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
   Constrexpr.constr_expr * Id.Set.t
 
 val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
+  (Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
     Constrexpr.constr_expr * Id.Set.t) ->
   constr_expr -> constr_expr * Id.Set.t
 
 (* Should be likely located elsewhere *)
-exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *)
-val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
+val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1d5142a5c2..61ed40394e 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -265,7 +265,7 @@ type 'a infos_cache = {
   i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
   i_env : env;
   i_sigma : existential -> constr option;
-  i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t;
+  i_rels : (Constr.rel_declaration * lazy_val) Range.t;
 }
 
 and 'a infos = {
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 45812b5a1e..9bf743152f 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1209,3 +1209,10 @@ let hcons =
      Id.hcons)
 
 (* let hcons_types = hcons_constr *)
+
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
+type rel_context = rel_declaration list
+type named_context = named_declaration list
+type compacted_context = compacted_declaration list
diff --git a/kernel/constr.mli b/kernel/constr.mli
index bf7b5e87b5..70acf19328 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -372,6 +372,15 @@ val eq_constr_nounivs : constr -> constr -> bool
 (** Total ordering compatible with [equal] *)
 val compare : constr -> constr -> int
 
+(** {6 Extension of Context with declarations on constr} *)
+
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
+type rel_context = rel_declaration list
+type named_context = named_declaration list
+type compacted_context = compacted_declaration list
+
 (** {6 Functionals working on the immediate subterm of a construction } *)
 
 (** [fold f acc c] folds [f] on the immediate subterms of [c]
diff --git a/kernel/context.ml b/kernel/context.ml
index 5d4a101840..831dc850fb 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -43,8 +43,6 @@ struct
       | LocalAssum of Name.t * 'types            (** name, type *)
       | LocalDef of Name.t * 'constr * 'types   (** name, value, type *)
 
-    type t = (Constr.constr, Constr.types) pt
-
     (** Return the name bound by a given declaration. *)
     let get_name = function
       | LocalAssum (na,_)
@@ -157,7 +155,6 @@ struct
       Inner-most declarations are at the beginning of the list.
       Outer-most declarations are at the end of the list. *)
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-  type t = Declaration.t list
 
   (** empty rel-context *)
   let empty = []
@@ -241,8 +238,6 @@ struct
       | LocalAssum of Id.t * 'types             (** identifier, type *)
       | LocalDef of Id.t * 'constr * 'types    (** identifier, value, type *)
 
-    type t = (Constr.constr, Constr.types) pt
-
     (** Return the identifier bound by a given declaration. *)
     let get_id = function
       | LocalAssum (id,_) -> id
@@ -370,7 +365,6 @@ struct
       Inner-most declarations are at the beginning of the list.
       Outer-most declarations are at the end of the list. *)
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-  type t = Declaration.t list
 
   (** empty named-context *)
   let empty = []
@@ -429,8 +423,6 @@ module Compacted =
           | LocalAssum of Id.t list * 'types
           | LocalDef of Id.t list * 'constr * 'types
 
-        type t = (Constr.constr, Constr.types) pt
-
         let map_constr f = function
           | LocalAssum (ids, ty) as decl ->
              let ty' = f ty in
@@ -454,7 +446,6 @@ module Compacted =
       end
 
     type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-    type t = Declaration.t list
 
     let fold f l ~init = List.fold_right f l init
   end
diff --git a/kernel/context.mli b/kernel/context.mli
index c97db4348e..957ac4b3d6 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -35,8 +35,6 @@ sig
     | LocalAssum of Name.t * 'types            (** name, type *)
     | LocalDef of Name.t * 'constr * 'types   (** name, value, type *)
 
-    type t = (Constr.constr, Constr.types) pt
-
     (** Return the name bound by a given declaration. *)
     val get_name : ('c, 't) pt -> Name.t
 
@@ -93,7 +91,6 @@ sig
       Inner-most declarations are at the beginning of the list.
       Outer-most declarations are at the end of the list. *)
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-  type t = Declaration.t list
 
   (** empty rel-context *)
   val empty : ('c, 't) pt
@@ -153,8 +150,6 @@ sig
       | LocalAssum of Id.t * 'types             (** identifier, type *)
       | LocalDef of Id.t * 'constr * 'types    (** identifier, value, type *)
 
-    type t = (Constr.constr, Constr.types) pt
-
     (** Return the identifier bound by a given declaration. *)
     val get_id : ('c, 't) pt -> Id.t
 
@@ -220,7 +215,6 @@ sig
       Inner-most declarations are at the beginning of the list.
       Outer-most declarations are at the end of the list. *)
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-  type t = Declaration.t list
 
   (** empty named-context *)
   val empty : ('c, 't) pt
@@ -270,15 +264,12 @@ sig
       | LocalAssum of Id.t list * 'types
       | LocalDef of Id.t list * 'constr * 'types
 
-    type t = (Constr.constr, Constr.types) pt
-
     val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
     val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt
     val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt
   end
 
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
-  type t = Declaration.t list
 
   val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a
 end
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index c7a84f6170..521a7d8901 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -157,7 +157,7 @@ type result = {
   cook_type : types;
   cook_universes : constant_universes;
   cook_inline : inline;
-  cook_context : Context.Named.t option;
+  cook_context : Constr.named_context option;
 }
 
 let on_body ml hy f = function
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 76c79335f1..4c254d2ea7 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -23,7 +23,7 @@ type result = {
   cook_type : types;
   cook_universes : constant_universes;
   cook_inline : inline;
-  cook_context : Context.Named.t option;
+  cook_context : Constr.named_context option;
 }
 
 val cook_constant : hcons:bool -> env -> recipe -> result
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 58fb5d66b7..95078800e7 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -80,7 +80,7 @@ type typing_flags = {
 (* some contraints are in constant_constraints, some other may be in
  * the OpaqueDef *)
 type constant_body = {
-    const_hyps : Context.Named.t; (** New: younger hyp at top *)
+    const_hyps : Constr.named_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
@@ -138,7 +138,7 @@ type one_inductive_body = {
 
     mind_typename : Id.t; (** Name of the type: [Ii] *)
 
-    mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
+    mind_arity_ctxt : Constr.rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
 
     mind_arity : inductive_arity; (** Arity sort and original user arity *)
 
@@ -196,13 +196,13 @@ type mutual_inductive_body = {
 
     mind_ntypes : int;  (** Number of types in the block *)
 
-    mind_hyps : Context.Named.t;  (** Section hypotheses on which the block depends *)
+    mind_hyps : Constr.named_context;  (** Section hypotheses on which the block depends *)
 
     mind_nparams : int;  (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *)
 
     mind_nparams_rec : int;  (** Number of recursively uniform (i.e. ordinary) parameters *)
 
-    mind_params_ctxt : Context.Rel.t;  (** The context of parameters (includes let-in declaration) *)
+    mind_params_ctxt : Constr.rel_context;  (** The context of parameters (includes let-in declaration) *)
 
     mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 724ed9ec7d..40873bea76 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -75,7 +75,7 @@ type 'a in_constant_universes_entry = 'a * constant_universes_entry
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
-  const_entry_secctx : Context.Named.t option;
+  const_entry_secctx : Constr.named_context option;
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
@@ -85,7 +85,7 @@ type 'a definition_entry = {
 
 type section_def_entry = {
   secdef_body : constr;
-  secdef_secctx : Context.Named.t option;
+  secdef_secctx : Constr.named_context option;
   secdef_feedback : Stateid.t option;
   secdef_type : types option;
 }
@@ -93,7 +93,7 @@ type section_def_entry = {
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
-    Context.Named.t option * types in_constant_universes_entry * inline
+    Constr.named_context option * types in_constant_universes_entry * inline
 
 type 'a constant_entry =
   | DefinitionEntry of 'a definition_entry
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0e34a71650..cc14dae5bb 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -76,13 +76,13 @@ let dummy_lazy_val () = ref VKnone
 let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
 
 type named_context_val = {
-  env_named_ctx : Context.Named.t;
-  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+  env_named_ctx : Constr.named_context;
+  env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
 }
 
 type rel_context_val = {
-  env_rel_ctx : Context.Rel.t;
-  env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
+  env_rel_ctx : Constr.rel_context;
+  env_rel_map : (Constr.rel_declaration * lazy_val) Range.t;
 }
 
 type env = {
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8928b32f1b..deca8afdeb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -60,13 +60,13 @@ type stratification = {
 }
 
 type named_context_val = private {
-  env_named_ctx : Context.Named.t;
-  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+  env_named_ctx : Constr.named_context;
+  env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
 }
 
 type rel_context_val = private {
-  env_rel_ctx : Context.Rel.t;
-  env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
+  env_rel_ctx : Constr.rel_context;
+  env_rel_map : (Constr.rel_declaration * lazy_val) Range.t;
 }
 
 type env = private {
@@ -88,8 +88,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
-val rel_context   : env -> Context.Rel.t
-val named_context : env -> Context.Named.t
+val rel_context   : env -> Constr.rel_context
+val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
 
 val opaque_tables : env -> Opaqueproof.opaquetab
@@ -108,13 +108,13 @@ val empty_context : env -> bool
 (** {5 Context of de Bruijn variables ([rel_context]) } *)
 
 val nb_rel           : env -> int
-val push_rel         : Context.Rel.Declaration.t -> env -> env
-val push_rel_context : Context.Rel.t -> env -> env
+val push_rel         : Constr.rel_declaration -> env -> env
+val push_rel_context : Constr.rel_context -> env -> env
 val push_rec_types   : rec_declaration -> env -> env
 
 (** Looks up in the context of local vars referred by indice ([rel_context]) 
    raises [Not_found] if the index points out of the context *)
-val lookup_rel    : int -> env -> Context.Rel.Declaration.t
+val lookup_rel    : int -> env -> Constr.rel_declaration
 val lookup_rel_val : int -> env -> lazy_val
 val evaluable_rel : int -> env -> bool
 val env_of_rel     : int -> env -> env
@@ -122,12 +122,12 @@ val env_of_rel     : int -> env -> env
 (** {6 Recurrence on [rel_context] } *)
 
 val fold_rel_context :
-  (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> Constr.rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (** {5 Context of variables (section variables and goal assumptions) } *)
 
-val named_context_of_val : named_context_val -> Context.Named.t
-val val_of_named_context : Context.Named.t -> named_context_val
+val named_context_of_val : named_context_val -> Constr.named_context
+val val_of_named_context : Constr.named_context -> named_context_val
 val empty_named_context_val : named_context_val
 val ids_of_named_context_val : named_context_val -> Id.Set.t
 
@@ -138,19 +138,19 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t
 val map_named_val :
    (constr -> constr) -> named_context_val -> named_context_val
 
-val push_named : Context.Named.Declaration.t -> env -> env
-val push_named_context : Context.Named.t -> env -> env
+val push_named : Constr.named_declaration -> env -> env
+val push_named_context : Constr.named_context -> env -> env
 val push_named_context_val  :
-    Context.Named.Declaration.t -> named_context_val -> named_context_val
+    Constr.named_declaration -> named_context_val -> named_context_val
 
 
 
 (** Looks up in the context of local vars referred by names ([named_context]) 
    raises [Not_found] if the Id.t is not found *)
 
-val lookup_named     : variable -> env -> Context.Named.Declaration.t
+val lookup_named     : variable -> env -> Constr.named_declaration
 val lookup_named_val : variable -> env -> lazy_val
-val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t
+val lookup_named_ctxt : variable -> named_context_val -> Constr.named_declaration
 val evaluable_named  : variable -> env -> bool
 val named_type : variable -> env -> types
 val named_body : variable -> env -> constr option
@@ -158,13 +158,13 @@ val named_body : variable -> env -> constr option
 (** {6 Recurrence on [named_context]: older declarations processed first } *)
 
 val fold_named_context :
-  (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
 val set_universes : env -> UGraph.t -> env
 
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
-  ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
+  ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
 
 (** This forgets named and rel contexts *)
 val reset_context : env -> env
@@ -280,7 +280,7 @@ val vars_of_global : env -> constr -> Id.Set.t
 val really_needed : env -> Id.Set.t -> Id.Set.t
 
 (** like [really_needed] but computes a well ordered named context *)
-val keep_hyps : env -> Id.Set.t -> Context.Named.t
+val keep_hyps : env -> Id.Set.t -> Constr.named_context
 
 (** {5 Unsafe judgments. }
     We introduce here the pre-type of judgments, which is
@@ -309,10 +309,10 @@ exception Hyp_not_found
    return [tail::(f head (id,_,_) (rev tail))::head].
    the value associated to id should not change *)
 val apply_to_hyp : named_context_val -> variable ->
-  (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) ->
+  (Constr.named_context -> Constr.named_declaration -> Constr.named_context -> Constr.named_declaration) ->
     named_context_val
 
-val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val
+val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val
 
 
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e63f43849a..61b71df31d 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -425,7 +425,7 @@ let typecheck_inductive env mie =
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
-  | LocalNotConstructor of Context.Rel.t * int
+  | LocalNotConstructor of Constr.rel_context * int
   | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c7982f1fc1..3c1464c6c9 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -36,7 +36,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 (** {6 Functions to build standard types related to inductive } *)
 val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list
 
-val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t
+val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_context
 
 val instantiate_inductive_constraints :
   mutual_inductive_body -> Instance.t -> Constraint.t
@@ -87,7 +87,7 @@ val build_branches_type :
     constr list -> constr -> types array
 
 (** Return the arity of an inductive type *)
-val mind_arity : one_inductive_body -> Context.Rel.t * Sorts.family
+val mind_arity : one_inductive_body -> Constr.rel_context * Sorts.family
 
 val inductive_sort_family : one_inductive_body -> Sorts.family
 
@@ -115,8 +115,8 @@ exception SingletonInductiveBecomesProp of Id.t
 
 val max_inductive_sort : Sorts.t array -> Universe.t
 
-val instantiate_universes : env -> Context.Rel.t ->
-  template_arity -> constr Lazy.t array -> Context.Rel.t * Sorts.t
+val instantiate_universes : env -> Constr.rel_context ->
+  template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t
 
 (** {6 Debug} *)
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 50713b9579..07a02f6ef5 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -5,8 +5,8 @@ UGraph
 Esubst
 Sorts
 Evar
-Constr
 Context
+Constr
 Vars
 Term
 Mod_subst
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index a484c08e8d..f8b71e4564 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -18,7 +18,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
+  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 type proofterm = (constr * Univ.ContextSet.t) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index b6ae80b46a..5ea6da649b 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -51,7 +51,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
+  abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 
 (* The type has two caveats:
    1) cook_constr is defined after
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index e53ab6aefb..581e8bd88a 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -116,10 +116,10 @@ val betazeta_appvect : int -> constr -> constr array -> constr
 (***********************************************************************
   s Recognizing products and arities modulo reduction *)
 
-val dest_prod       : env -> types -> Context.Rel.t * types
-val dest_prod_assum : env -> types -> Context.Rel.t * types
-val dest_lam        : env -> types -> Context.Rel.t * constr
-val dest_lam_assum  : env -> types -> Context.Rel.t * types
+val dest_prod       : env -> types -> Constr.rel_context * types
+val dest_prod_assum : env -> types -> Constr.rel_context * types
+val dest_lam        : env -> constr -> Constr.rel_context * constr
+val dest_lam_assum  : env -> constr -> Constr.rel_context * constr
 
 exception NotArity
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 81e344e73a..4851a9c0d0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -336,7 +336,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t)
    Such a term can canonically be seen as the pair of a context of types
    and of a sort *)
 
-type arity = Context.Rel.t * Sorts.t
+type arity = Constr.rel_context * Sorts.t
 
 let destArity =
   let open Context.Rel.Declaration in
diff --git a/kernel/term.mli b/kernel/term.mli
index 4d340399d3..181d714ed7 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -25,14 +25,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
 val mkNamedProd : Id.t -> types -> types -> types
 
 (** Constructs either [(x:t)c] or [[x=b:t]c] *)
-val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
-val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
-val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types
-val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types
+val mkProd_or_LetIn : Constr.rel_declaration -> types -> types
+val mkProd_wo_LetIn : Constr.rel_declaration -> types -> types
+val mkNamedProd_or_LetIn : Constr.named_declaration -> types -> types
+val mkNamedProd_wo_LetIn : Constr.named_declaration -> types -> types
 
 (** Constructs either [[x:t]c] or [[x=b:t]c] *)
-val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr
-val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr
+val mkLambda_or_LetIn : Constr.rel_declaration -> constr -> constr
+val mkNamedLambda_or_LetIn : Constr.named_declaration -> constr -> constr
 
 (** {5 Other term constructors. } *)
 
@@ -74,8 +74,8 @@ val to_lambda : int -> constr -> constr
    where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *)
 val to_prod : int -> constr -> constr
 
-val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
-val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn : constr -> Constr.rel_context -> constr
+val it_mkProd_or_LetIn : types -> Constr.rel_context -> types
 
 (** In [lambda_applist c args], [c] is supposed to have the form
     [λΓ.c] with [Γ] without let-in; it returns [c] with the variables
@@ -126,29 +126,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
    "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
-val decompose_prod_assum : types -> Context.Rel.t * types
+val decompose_prod_assum : types -> Constr.rel_context * types
 
 (** Idem with lambda's and let's *)
-val decompose_lam_assum : constr -> Context.Rel.t * constr
+val decompose_lam_assum : constr -> Constr.rel_context * constr
 
 (** Idem but extract the first [n] premisses, counting let-ins. *)
-val decompose_prod_n_assum : int -> types -> Context.Rel.t * types
+val decompose_prod_n_assum : int -> types -> Constr.rel_context * types
 
 (** Idem for lambdas, _not_ counting let-ins *)
-val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr
+val decompose_lam_n_assum : int -> constr -> Constr.rel_context * constr
 
 (** Idem, counting let-ins *)
-val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr
+val decompose_lam_n_decls : int -> constr -> Constr.rel_context * constr
 
 (** Return the premisses/parameters of a type/term (let-in included) *)
-val prod_assum : types -> Context.Rel.t
-val lam_assum : constr -> Context.Rel.t
+val prod_assum : types -> Constr.rel_context
+val lam_assum : constr -> Constr.rel_context
 
 (** Return the first n-th premisses/parameters of a type (let included and counted) *)
-val prod_n_assum : int -> types -> Context.Rel.t
+val prod_n_assum : int -> types -> Constr.rel_context
 
 (** Return the first n-th premisses/parameters of a term (let included but not counted) *)
-val lam_n_assum : int -> constr -> Context.Rel.t
+val lam_n_assum : int -> constr -> Constr.rel_context
 
 (** Remove the premisses/parameters of a type/term *)
 val strip_prod : types -> types
@@ -167,7 +167,7 @@ val strip_lam_assum : constr -> constr
     Such a term can canonically be seen as the pair of a context of types
     and of a sort *)
 
-type arity = Context.Rel.t * Sorts.t
+type arity = Constr.rel_context * Sorts.t
 
 (** Build an "arity" from its canonical form *)
 val mkArity : arity -> types
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 3b2abc7771..57acdfe4b5 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -28,7 +28,7 @@ val infer_v    : env -> constr array -> unsafe_judgment array
 val infer_type : env -> types        -> unsafe_type_judgment
 
 val infer_local_decls :
-  env -> (Id.t * local_entry) list -> (env * Context.Rel.t)
+  env -> (Id.t * local_entry) list -> (env * Constr.rel_context)
 
 (** {6 Basic operations of the typing machine. } *)
 
@@ -102,4 +102,4 @@ val judge_of_case : env -> case_info
 val type_of_constant_in : env -> pconstant -> types
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit
+val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit
diff --git a/kernel/vars.mli b/kernel/vars.mli
index a0c7ba4bd2..fdddbdb342 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -70,10 +70,10 @@ type substl = constr list
    as if usable in [applist] while the substitution is
    represented the other way round, i.e. ending with either [u₁] or
    [c₁], as if usable for [substl]. *)
-val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl
+val subst_of_rel_context_instance : Constr.rel_context -> constr list -> substl
 
 (** For compatibility: returns the substitution reversed *)
-val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
+val adjust_subst_to_rel_context : Constr.rel_context -> constr list -> constr list
 
 (** Take an index in an instance of a context and returns its index wrt to
     the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *)
@@ -97,13 +97,13 @@ val subst1 : constr -> constr -> constr
     accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if
     Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then
     Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *)
-val substnl_decl : substl -> int -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
+val substnl_decl : substl -> int -> Constr.rel_declaration -> Constr.rel_declaration
 
 (** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *)
-val substl_decl : substl -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
+val substl_decl : substl -> Constr.rel_declaration -> Constr.rel_declaration
 
 (** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *)
-val subst1_decl : constr -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
+val subst1_decl : constr -> Constr.rel_declaration -> Constr.rel_declaration
 
 (** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by
     [cj] in [t]. *)
@@ -134,8 +134,8 @@ open Univ
 (** Level substitutions for polymorphism. *)
 
 val subst_univs_level_constr : universe_level_subst -> constr -> constr
-val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t
+val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context -> Constr.rel_context
 
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Instance.t -> constr -> constr
-val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t
+val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context
diff --git a/library/global.mli b/library/global.mli
index 57e173cb93..b2a191ceeb 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -23,7 +23,7 @@ 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 } *)
 
@@ -79,7 +79,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
diff --git a/library/lib.ml b/library/lib.ml
index 128b27e757..a20de55bf6 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -405,7 +405,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 = {
diff --git a/library/lib.mli b/library/lib.mli
index 1d77212e9d..5abfccfc7d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Names
+
 (** Lib: record of operations, backtrack, low-level sections *)
 
 (** This module provides a general mechanism to keep a trace of all operations
@@ -153,7 +154,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;
@@ -165,7 +166,7 @@ type abstr_info = private {
 }
 
 val instance_from_variable_context : variable_context -> Id.t array
-val named_of_variable_context : variable_context -> Context.Named.t
+val named_of_variable_context : variable_context -> Constr.named_context
 
 val section_segment_of_constant : Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
@@ -179,9 +180,9 @@ val is_in_section : GlobRef.t -> bool
 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 ->
-  Constant.t -> Context.Named.t -> unit
+  Constant.t -> Constr.named_context -> unit
 val add_section_kn : Decl_kinds.polymorphic ->
-  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 } *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d599afe699..64407f3595 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -303,7 +303,7 @@ type constructor_summary = {
   cs_cstr : pconstructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : Context.Rel.t;
+  cs_args : Constr.rel_context;
   cs_concl_realargs : constr array
 }
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index aa53f7e67c..8eaef24c48 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -93,12 +93,12 @@ val inductive_nparamdecls : inductive -> int
 val inductive_nparamdecls_env : env -> inductive -> int
 
 (** @return params context *)
-val inductive_paramdecls : pinductive -> Context.Rel.t
-val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t
+val inductive_paramdecls : pinductive -> Constr.rel_context
+val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context
 
 (** @return full arity context, hence with letin *)
-val inductive_alldecls : pinductive -> Context.Rel.t
-val inductive_alldecls_env : env -> pinductive -> Context.Rel.t
+val inductive_alldecls : pinductive -> Constr.rel_context
+val inductive_alldecls_env : env -> pinductive -> Constr.rel_context
 
 (** {7 Extract information from a constructor name} *)
 
@@ -141,7 +141,7 @@ type constructor_summary = {
   cs_cstr : pconstructor;    (* internal name of the constructor plus universes *)
   cs_params : constr list;   (* parameters of the constructor in current ctx *)
   cs_nargs : int;            (* length of arguments signature (letin included) *)
-  cs_args : Context.Rel.t;   (* signature of the arguments (letin included) *)
+  cs_args : Constr.rel_context;   (* signature of the arguments (letin included) *)
   cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *)
 }
 val lift_constructor : int -> constructor_summary -> constructor_summary
@@ -154,7 +154,7 @@ val get_projections  : env -> inductive_family -> Constant.t array option
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
     part of the inductive family, they appears in the arity *)
-val get_arity        : env -> inductive_family -> Context.Rel.t * Sorts.family
+val get_arity        : env -> inductive_family -> Constr.rel_context * Sorts.family
 
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d3aa7ac643..efb3c339ac 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -74,10 +74,10 @@ type typeclass = {
   cl_impl : GlobRef.t;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : GlobRef.t option list * Context.Rel.t;
+  cl_context : GlobRef.t option list * Constr.rel_context;
 
   (* Context of definitions and properties on defs, will not be shared *)
-  cl_props : Context.Rel.t;
+  cl_props : Constr.rel_context;
 
   (* The method implementaions as projections. *)
   cl_projs : (Name.t * (direction * hint_info) option
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e4a56960cf..80c6d82397 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -35,10 +35,10 @@ type typeclass = {
 
   (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
       The global reference gives a direct link to the class itself. *)
-  cl_context : GlobRef.t option list * Context.Rel.t;
+  cl_context : GlobRef.t option list * Constr.rel_context;
 
   (** Context of definitions and properties on defs, will not be shared *)
-  cl_props : Context.Rel.t;
+  cl_props : Constr.rel_context;
 
   (** The methods implementations of the typeclass as projections. 
       Some may be undefinable due to sorting restrictions or simply undefined if 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f926e82751..fd7135b6a6 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -40,7 +40,7 @@ type object_pr = {
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
   print_modtype             : ModPath.t -> Pp.t;
-  print_named_decl          : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t;
+  print_named_decl          : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
   print_library_entry       : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
   print_context             : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
   print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 8dd7296100..1668bce297 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -89,7 +89,7 @@ type object_pr = {
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
   print_modtype             : ModPath.t -> Pp.t;
-  print_named_decl          : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t;
+  print_named_decl          : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
   print_library_entry       : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
   print_context             : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
   print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index d76bd1e2b2..92224c992c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -852,7 +852,7 @@ type axiom =
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+  | Axiom of axiom * (Label.t * Constr.rel_context * types) list
   | Opaque of Constant.t     (* An opaque constant. *)
   | Transparent of Constant.t
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 7a8b963d25..eddfef6fad 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -152,13 +152,13 @@ val get_compact_context : unit -> bool
 val pr_context_unlimited   : env -> evar_map -> Pp.t
 val pr_ne_context_of       : Pp.t -> env -> evar_map -> Pp.t
 
-val pr_named_decl          : env -> evar_map -> Context.Named.Declaration.t -> Pp.t
-val pr_compacted_decl      : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t
-val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t
+val pr_named_decl          : env -> evar_map -> Constr.named_declaration -> Pp.t
+val pr_compacted_decl      : env -> evar_map -> Constr.compacted_declaration -> Pp.t
+val pr_rel_decl            : env -> evar_map -> Constr.rel_declaration -> Pp.t
 
-val pr_named_context       : env -> evar_map -> Context.Named.t -> Pp.t
+val pr_named_context       : env -> evar_map -> Constr.named_context -> Pp.t
 val pr_named_context_of    : env -> evar_map -> Pp.t
-val pr_rel_context         : env -> evar_map -> Context.Rel.t -> Pp.t
+val pr_rel_context         : env -> evar_map -> Constr.rel_context -> Pp.t
 val pr_rel_context_of      : env -> evar_map -> Pp.t
 val pr_context_of          : env -> evar_map -> Pp.t
 
@@ -210,7 +210,7 @@ type axiom =
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+  | Axiom of axiom * (Label.t * Constr.rel_context * types) list
   | Opaque of Constant.t     (* An opaque constant. *)
   | Transparent of Constant.t
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 47c9c51ee1..7e250faa86 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -93,7 +93,7 @@ type pstate = {
   pid : Id.t;  (* the name of the theorem whose proof is being constructed *)
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
-  section_vars : Context.Named.t option;
+  section_vars : Constr.named_context option;
   proof : Proof.t;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 9e07ed2d05..854ceaa41a 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -126,8 +126,8 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
 val set_used_variables :
-  Names.Id.t list -> Context.Named.t * Names.lident list
-val get_used_variables : unit -> Context.Named.t option
+  Names.Id.t list -> Constr.named_context * Names.lident list
+val get_used_variables : unit -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : unit -> UState.universe_decl
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 0e2b0c80e8..751e79d89c 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -23,7 +23,7 @@ open Printer
 val traverse :
   Label.t -> constr ->
     (Refset_env.t * Refset_env.t Refmap_env.t *
-     (Label.t * Context.Rel.t * types) list Refmap_env.t)
+     (Label.t * Constr.rel_context * types) list Refmap_env.t)
 
 (** Collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type). The above warning of
diff --git a/vernac/classes.mli b/vernac/classes.mli
index bd30b2d60e..9c37364cb0 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -16,9 +16,9 @@ open Libnames
 
 (** Errors *)
 
-val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
+val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a
 
-val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
+val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a
 
 (** Instance declaration *)
 
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index f51bfbad59..b1a9c8a5a3 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -82,12 +82,12 @@ val interp_fixpoint :
 val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
-  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
+  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
-  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
+  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
 (** Very private function, do not use *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 1d38075022..91caddcf13 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -25,7 +25,7 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
 
 val explain_inductive_error : inductive_error -> Pp.t
 
-val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t
+val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t
 
 val explain_typeclass_error : env -> typeclass_error -> Pp.t
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index fa6a9adf1b..1f401b4e15 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -40,7 +40,7 @@ let check_evars env evm =
 
 type oblinfo =
   { ev_name: int * Id.t;
-    ev_hyps: Context.Named.t;
+    ev_hyps: Constr.named_context;
     ev_status: bool * Evar_kinds.obligation_definition_status;
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
diff --git a/vernac/record.mli b/vernac/record.mli
index b2c039f0b5..f46f59c14d 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -22,7 +22,7 @@ val declare_projections :
   bool list ->
   UnivNames.universe_binders ->
   Impargs.manual_implicits list ->
-  Context.Rel.t ->
+  Constr.rel_context ->
     (Name.t * bool) list * Constant.t option list
 
 val definition_structure :