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

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 0e34a7165..cc14dae5b 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 8928b32f1..deca8afde 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 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