3 files changed, 5 insertions, 7 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b797e455c..ff8ca0b7c 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Termops
 open Environ
 open Libnames
@@ -42,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
-  rel_context -> local_binder list
+  Context.Rel.t -> local_binder list
 
 (** Printing options *)
 val print_implicits : bool ref
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f9de8c466..68bc0b109 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -101,7 +101,7 @@ let global_reference id =
 
 let construct_reference ctx id =
   try
-    Term.mkVar (let _ = Context.lookup_named id ctx in id)
+    Term.mkVar (let _ = Context.Named.lookup id ctx in id)
   with Not_found ->
     global_reference id
 
@@ -685,7 +685,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
       str "variable " ++ pr_id id ++ str " should be bound to a term.")
   else
     (* Is [id] a goal or section variable *)
-    let _ = Context.lookup_named id namedctx in
+    let _ = Context.Named.lookup id namedctx in
       try
 	(* [id] a section variable *)
 	(* Redundant: could be done in intern_qualid *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b671c9881..c851fbb36 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Evd
 open Environ
 open Libnames
@@ -161,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map ref -> local_binder list ->
-  internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+  internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits)
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
@@ -178,7 +177,7 @@ val interp_context_evars :
 
 val locate_reference :  Libnames.qualid -> Globnames.global_reference
 val is_global : Id.t -> bool
-val construct_reference : named_context -> Id.t -> constr
+val construct_reference : Context.Named.t -> Id.t -> constr
 val global_reference : Id.t -> constr
 val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr