Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr

21 files changed, 92 insertions, 94 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1d5142a5c..61ed40394 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 45812b5a1..9bf743152 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 bf7b5e87b..70acf1932 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 5d4a10184..831dc850f 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 c97db4348..957ac4b3d 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 c7a84f617..521a7d890 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 76c79335f..4c254d2ea 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 58fb5d66b..95078800e 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 724ed9ec7..40873bea7 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 224b6d5b8..4ab469803 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -77,13 +77,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 084d3c4de..0259dbbdd 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -55,13 +55,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 {
@@ -83,8 +83,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
@@ -103,13 +103,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
@@ -117,12 +117,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
 
@@ -133,19 +133,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
@@ -153,13 +153,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
@@ -278,7 +278,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
@@ -307,10 +307,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 e63f43849..61b71df31 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 c7982f1fc..3c1464c6c 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 50713b957..07a02f6ef 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 a484c08e8..f8b71e456 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 b6ae80b46..5ea6da649 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 e53ab6aef..581e8bd88 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 81e344e73..4851a9c0d 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 4d340399d..181d714ed 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 3b2abc777..57acdfe4b 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 a0c7ba4bd..fdddbdb34 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