Merging Context and Sign.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 142 insertions, 192 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 2628895eb..49fd1ae8e 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -262,7 +262,7 @@ let evar_value info ev =
 
 let defined_vars flags env =
 (*  if red_local_const (snd flags) then*)
-    Sign.fold_named_context
+    Context.fold_named_context
       (fun (id,b,_) e ->
 	 match b with
 	   | None -> e
diff --git a/kernel/context.ml b/kernel/context.ml
index 4bc268da1..d24922e18 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -6,6 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Jean-Christophe Filliâtre out of names.ml as part of the
+   rebuilding of Coq around a purely functional abstract type-checker,
+   Aug 1999 *)
+(* Miscellaneous extensions, restructurations and bug-fixes by Hugo
+   Herbelin and Bruno Barras *)
+
+(* This file defines types and combinators regarding indexes-based and
+   names-based contexts *)
+
+open Util
 open Names
 
 (***************************************************************************)
@@ -62,3 +72,53 @@ let rel_context_nhyps hyps =
     | (_,None,_)::hyps -> nhyps (1+acc) hyps
     | (_,Some _,_)::hyps -> nhyps acc hyps in
   nhyps 0 hyps
+
+(*s Signatures of named hypotheses. Used for section variables and
+    goal assumptions. *)
+
+type named_context = named_declaration list
+
+let empty_named_context = []
+
+let add_named_decl d sign = d::sign
+
+let rec lookup_named id = function
+  | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
+  | _ :: sign -> lookup_named id sign
+  | [] -> raise Not_found
+
+let named_context_length = List.length
+let named_context_equal = List.equal eq_named_declaration
+
+let vars_of_named_context = List.map (fun (id,_,_) -> id)
+
+let instance_from_named_context sign =
+  let rec inst_rec = function
+    | (id,None,_) :: sign -> Constr.mkVar id :: inst_rec sign
+    | _ :: sign -> inst_rec sign
+    | [] -> [] in
+  Array.of_list (inst_rec sign)
+
+let fold_named_context f l ~init = List.fold_right f l init
+let fold_named_context_reverse f ~init l = List.fold_left f init l
+
+(*s Signatures of ordered section variables *)
+type section_context = named_context
+
+let fold_rel_context f l ~init:x = List.fold_right f l x
+let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
+
+let map_context f l =
+  let map_decl (n, body_o, typ as decl) =
+    let body_o' = Option.smartmap f body_o in
+    let typ' = f typ in
+      if body_o' == body_o && typ' == typ then decl else
+        (n, body_o', typ')
+  in
+    List.smartmap map_decl l
+
+let map_rel_context = map_context
+let map_named_context = map_context
+
+let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
diff --git a/kernel/context.mli b/kernel/context.mli
index 32efb743a..79ddbe49b 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -8,7 +8,9 @@
 
 open Names
 
-(** {6 Local } *)
+(** TODO: cleanup *)
+
+(** {6 Declarations} *)
 (** A {e declaration} has the form [(name,body,type)]. It is either an
     {e assumption} if [body=None] or a {e definition} if
     [body=Some actualbody]. It is referred by {e name} if [na] is an
@@ -45,10 +47,61 @@ val eq_named_declaration :
 val eq_rel_declaration :
     rel_declaration -> rel_declaration -> bool
 
-(** {6 Contexts of declarations referred to by de Bruijn indices } *)
+(** {6 Signatures of ordered named declarations } *)
 
-(** In [rel_context], more recent declaration is on top *)
+type named_context = named_declaration list
+type section_context = named_context
 type rel_context = rel_declaration list
+(** In [rel_context], more recent declaration is on top *)
+
+val empty_named_context : named_context
+val add_named_decl : named_declaration -> named_context -> named_context
+val vars_of_named_context : named_context -> Id.t list
+
+val lookup_named : Id.t -> named_context -> named_declaration
+
+(** number of declarations *)
+val named_context_length : named_context -> int
+
+(** named context equality *)
+val named_context_equal : named_context -> named_context -> bool
+
+(** {6 Recurrence on [named_context]: older declarations processed first } *)
+val fold_named_context :
+  (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
+
+(** newer declarations first *)
+val fold_named_context_reverse :
+  ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
+
+(** {6 Section-related auxiliary functions } *)
+val instance_from_named_context : named_context -> Constr.t array
+
+(** {6 ... } *)
+(** Signatures of ordered optionally named variables, intended to be
+   accessed by de Bruijn indices *)
+
+(** {6 Recurrence on [rel_context]: older declarations processed first } *)
+val fold_rel_context :
+  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+
+(** newer declarations first *)
+val fold_rel_context_reverse :
+  ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
+
+(** {6 Map function of [rel_context] } *)
+val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context
+
+(** {6 Map function of [named_context] } *)
+val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context
+
+(** {6 Map function of [rel_context] } *)
+val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit
+
+(** {6 Map function of [named_context] } *)
+val iter_named_context : (Constr.t -> unit) -> named_context -> unit
+
+(** {6 Contexts of declarations referred to by de Bruijn indices } *)
 
 val empty_rel_context : rel_context
 val add_rel_decl : rel_declaration -> rel_context -> rel_context
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0851f682d..bb29b9645 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -18,7 +18,6 @@ open Util
 open Names
 open Term
 open Context
-open Sign
 open Declarations
 open Environ
 
@@ -124,7 +123,7 @@ type inline = bool
 
 type result =
   constant_def * constant_type * Univ.constraints * inline
-    * Sign.section_context option
+    * Context.section_context option
 
 let on_body f = function
   | Undef inl -> Undef inl
@@ -139,13 +138,13 @@ let constr_of_def = function
 
 let cook_constant env r =
   let cb = r.d_from in
-  let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
+  let hyps = Context.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
   let body = on_body
     (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps)
     cb.const_body
   in
   let const_hyps =
-    Sign.fold_named_context (fun (h,_,_) hyps ->
+    Context.fold_named_context (fun (h,_,_) hyps ->
       List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps)
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index d6280e119..8d046a12e 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,14 +18,14 @@ type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
 
 type recipe = {
   d_from : constant_body;
-  d_abstract : Sign.named_context;
+  d_abstract : Context.named_context;
   d_modlist : work_list }
 
 type inline = bool
 
 type result =
   constant_def * constant_type * constraints * inline
-    * Sign.section_context option
+    * Context.section_context option
 
 val cook_constant : env -> recipe -> result
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index d00a20a80..146b6a1ec 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -115,7 +115,7 @@ and slot_for_fv env fv =
 	match !nv with
 	| VKvalue (v,_) -> v
 	| VKnone ->
-	    let (_, b, _) = Sign.lookup_named id env.env_named_context in
+	    let (_, b, _) = Context.lookup_named id env.env_named_context in
 	    let v,d =
 	      match b with
 		| None -> (val_of_named id, Id.Set.empty)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 5d9eaa928..24572da59 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -47,7 +47,7 @@ type native_name =
   | NotLinked
 
 type constant_body = {
-    const_hyps : Sign.section_context; (** New: younger hyp at top *)
+    const_hyps : Context.section_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted;
@@ -132,7 +132,7 @@ type mutual_inductive_body = {
 
     mind_ntypes : int;  (** Number of types in the block *)
 
-    mind_hyps : Sign.section_context;  (** Section hypotheses on which the block depends *)
+    mind_hyps : Context.section_context;  (** Section hypotheses on which the block depends *)
 
     mind_nparams : int;  (** Number of expected parameters *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3c1f6a415..64496033a 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -166,7 +166,7 @@ let subst_mind sub mib =
     mind_nparams = mib.mind_nparams;
     mind_nparams_rec = mib.mind_nparams_rec;
     mind_params_ctxt =
-      Sign.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
+      Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_constraints = mib.mind_constraints;
     mind_native_name = ref NotLinked }
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 650c3566d..b2d65d3ed 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -50,14 +50,14 @@ type mutual_inductive_entry = {
 
 type definition_entry = {
   const_entry_body   : constr;
-  const_entry_secctx : Sign.section_context option;
+  const_entry_secctx : Context.section_context option;
   const_entry_type        : types option;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
 type inline = int option (* inlining level, None for no inlining *)
 
-type parameter_entry = Sign.section_context option * types * inline
+type parameter_entry = Context.section_context option * types * inline
 
 type constant_entry =
   | DefinitionEntry of definition_entry
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d3b223505..4a3e51aa1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -25,7 +25,6 @@ open Util
 open Names
 open Term
 open Context
-open Sign
 open Vars
 open Univ
 open Declarations
@@ -68,7 +67,7 @@ let nb_rel env = env.env_nb_rel
 
 let push_rel = push_rel
 
-let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
+let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
   let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
@@ -110,8 +109,8 @@ let val_of_named_context ctxt =
   List.fold_right push_named_context_val ctxt empty_named_context_val
 
 
-let lookup_named id env = Sign.lookup_named id env.env_named_context
-let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt
+let lookup_named id env = Context.lookup_named id env.env_named_context
+let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt
 
 let eq_named_context_val c1 c2 =
    c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2)
@@ -150,7 +149,7 @@ let fold_named_context f env ~init =
   in fold_right env
 
 let fold_named_context_reverse f ~init env =
-  Sign.fold_named_context_reverse f ~init:init (named_context env)
+  Context.fold_named_context_reverse f ~init:init (named_context env)
 
 (* Global constants *)
 
@@ -216,11 +215,11 @@ let set_engagement c env = (* Unsafe *)
 (* Lookup of section variables *)
 let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
-  Sign.vars_of_named_context cmap.const_hyps
+  Context.vars_of_named_context cmap.const_hyps
 
 let lookup_inductive_variables (kn,i) env =
   let mis = lookup_mind kn env in
-  Sign.vars_of_named_context mis.mind_hyps
+  Context.vars_of_named_context mis.mind_hyps
 
 let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
@@ -254,7 +253,7 @@ let global_vars_set env constr =
 
 let keep_hyps env needed =
   let really_needed =
-    Sign.fold_named_context_reverse
+    Context.fold_named_context_reverse
       (fun need (id,copt,t) ->
         if Id.Set.mem id need then
           let globc =
@@ -267,7 +266,7 @@ let keep_hyps env needed =
         else need)
       ~init:needed
       (named_context env) in
-  Sign.fold_named_context
+  Context.fold_named_context
     (fun (id,_,_ as d) nsign ->
       if Id.Set.mem id really_needed then add_named_decl d nsign
       else nsign)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ffe28ddc4..ffa3ceb87 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -10,7 +10,6 @@ open Names
 open Term
 open Context
 open Declarations
-open Sign
 
 (** Unsafe environments. We define here a datatype for environments.
    Since typing is not yet defined, it is not possible to check the
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ef4416061..ee311ab24 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -68,7 +68,7 @@ let instantiate_params full t args sign =
   let fail () =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
-    Sign.fold_rel_context
+    Context.fold_rel_context
       (fun (_,copt,_) (largs,subs,ty) ->
         match (copt, largs, kind_of_term ty) with
           | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
@@ -240,7 +240,7 @@ let type_of_constructors ind (mib,mip) =
 
 let local_rels ctxt =
   let (rels,_) =
-    Sign.fold_rel_context_reverse
+    Context.fold_rel_context_reverse
       (fun (rels,n) (_,copt,_) ->
         match copt with
             None   -> (mkRel n :: rels, n+1)
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 421003560..36b3d8323 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -7,7 +7,6 @@ Context
 Vars
 Term
 Mod_subst
-Sign
 Cbytecodes
 Copcodes
 Cemitcodes
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index f112393cd..20593744b 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -14,7 +14,6 @@ open Util
 open Nativevalues
 open Nativelambda
 open Pre_env
-open Sign
 
 (** This file defines the mllambda code generation phase of the native
 compiler. mllambda represents a fragment of ML, and can easily be printed
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 922fbae92..61fb6b07b 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -16,7 +16,6 @@
 open Util
 open Names
 open Context
-open Sign
 open Univ
 open Term
 open Declarations
@@ -105,7 +104,7 @@ let env_of_rel n env =
 let push_named_context_val d (ctxt,vals) =
   let id,_,_ = d in
   let rval = ref VKnone in
-    Sign.add_named_decl d ctxt, (id,rval)::vals
+    Context.add_named_decl d ctxt, (id,rval)::vals
 
 let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
@@ -113,7 +112,7 @@ let push_named d env =
   let id,body,_ = d in
   let rval = ref VKnone in
     { env with
-      env_named_context = Sign.add_named_decl d env.env_named_context;
+      env_named_context = Context.add_named_decl d env.env_named_context;
       env_named_vals =  (id,rval):: env.env_named_vals }
 
 let lookup_named_val id env =
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index d3d500b2c..10c9c27cb 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Sign
 open Univ
 open Term
 open Context
diff --git a/kernel/sign.ml b/kernel/sign.ml
deleted file mode 100644
index 66c872f12..000000000
--- a/kernel/sign.ml
+++ /dev/null
@@ -1,88 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Created by Jean-Christophe Filliâtre out of names.ml as part of the
-   rebuilding of Coq around a purely functional abstract type-checker,
-   Aug 1999 *)
-(* Miscellaneous extensions, restructurations and bug-fixes by Hugo
-   Herbelin and Bruno Barras *)
-
-(* This file defines types and combinators regarding indexes-based and
-   names-based contexts *)
-
-open Names
-open Util
-open Term
-open Context
-
-(*s Signatures of named hypotheses. Used for section variables and
-    goal assumptions. *)
-
-type named_context = named_declaration list
-
-let empty_named_context = []
-
-let add_named_decl d sign = d::sign
-
-let rec lookup_named id = function
-  | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
-  | _ :: sign -> lookup_named id sign
-  | [] -> raise Not_found
-
-let named_context_length = List.length
-let named_context_equal = List.equal eq_named_declaration
-
-let vars_of_named_context = List.map (fun (id,_,_) -> id)
-
-let instance_from_named_context sign =
-  let rec inst_rec = function
-    | (id,None,_) :: sign -> mkVar id :: inst_rec sign
-    | _ :: sign -> inst_rec sign
-    | [] -> [] in
-  Array.of_list (inst_rec sign)
-
-let fold_named_context f l ~init = List.fold_right f l init
-let fold_named_context_reverse f ~init l = List.fold_left f init l
-
-(*s Signatures of ordered section variables *)
-type section_context = named_context
-
-let fold_rel_context f l ~init:x = List.fold_right f l x
-let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
-
-let map_context f l =
-  let map_decl (n, body_o, typ as decl) =
-    let body_o' = Option.smartmap f body_o in
-    let typ' = f typ in
-      if body_o' == body_o && typ' == typ then decl else
-	(n, body_o', typ')
-  in
-    List.smartmap map_decl l
-
-let map_rel_context = map_context
-let map_named_context = map_context
-
-let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-
-(* Push named declarations on top of a rel context *)
-(* Bizarre. Should be avoided. *)
-(*let push_named_to_rel_context hyps ctxt =
-  let rec push = function
-    | (id,b,t) :: l ->
-	let s, hyps = push l in
-	let d = (Name id, Option.map (subst_vars s) b, subst_vars s t) in
-	id::s, d::hyps
-    | [] -> [],[] in
-  let s, hyps = push hyps in
-  let rec subst = function
-    | d :: l ->
-	let n, ctxt = subst l in
-	(n+1), (map_rel_declaration (substn_vars n s) d)::ctxt
-    | [] -> 1, hyps in
-  snd (subst ctxt)*)
diff --git a/kernel/sign.mli b/kernel/sign.mli
deleted file mode 100644
index 6e581df34..000000000
--- a/kernel/sign.mli
+++ /dev/null
@@ -1,67 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Context
-
-(** TODO: Merge this with Context *)
-
-(** {6 Signatures of ordered named declarations } *)
-
-type named_context = named_declaration list
-type section_context = named_context
-
-val empty_named_context : named_context
-val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> Id.t list
-
-val lookup_named : Id.t -> named_context -> named_declaration
-
-(** number of declarations *)
-val named_context_length : named_context -> int
-
-(** named context equality *)
-val named_context_equal : named_context -> named_context -> bool
-
-(** {6 Recurrence on [named_context]: older declarations processed first } *)
-val fold_named_context :
-  (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
-
-(** newer declarations first *)
-val fold_named_context_reverse :
-  ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
-
-(** {6 Section-related auxiliary functions } *)
-val instance_from_named_context : named_context -> constr array
-
-(** {6 ... } *)
-(** Signatures of ordered optionally named variables, intended to be
-   accessed by de Bruijn indices *)
-
-(* val push_named_to_rel_context : named_context -> rel_context -> rel_context *)
-
-(** {6 Recurrence on [rel_context]: older declarations processed first } *)
-val fold_rel_context :
-  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
-
-(** newer declarations first *)
-val fold_rel_context_reverse :
-  ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
-
-(** {6 Map function of [rel_context] } *)
-val map_rel_context : (constr -> constr) -> rel_context -> rel_context
-
-(** {6 Map function of [named_context] } *)
-val map_named_context : (constr -> constr) -> named_context -> named_context
-
-(** {6 Map function of [rel_context] } *)
-val iter_rel_context : (constr -> unit) -> rel_context -> unit
-
-(** {6 Map function of [named_context] } *)
-val iter_named_context : (constr -> unit) -> named_context -> unit
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3653e1954..83d1ce16c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -76,7 +76,7 @@ let infer_declaration env = function
 let global_vars_set_constant_type env = function
   | NonPolymorphicType t -> global_vars_set env t
   | PolymorphicArity (ctx,_) ->
-      Sign.fold_rel_context
+      Context.fold_rel_context
         (fold_rel_declaration
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a27ce1c47..cc7cf0c68 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -97,7 +97,7 @@ let judge_of_variable env id =
    variables of the current env *)
 (* TODO: check order? *)
 let check_hyps_inclusion env c sign =
-  Sign.fold_named_context
+  Context.fold_named_context
     (fun (id,_,ty1) () ->
       try
         let ty2 = named_type id env in
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 240d4d413..55a28516b 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Context
-open Sign
 
 (** {6 Occur checks } *)