4 files changed, 16 insertions, 16 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 913825a9f..ecb36615f 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 8ce1b625f..135aa73fc 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 64db70451..d638bb2d3 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 f9aa6ba63..80988989f 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