Merging Context and Sign.

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

86 files changed, 210 insertions, 282 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index b09c8e97e..0f1686000 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -46,7 +46,6 @@ Context
 Vars
 Term
 Mod_subst
-Sign
 Cbytecodes
 Copcodes
 Cemitcodes
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 4cf79337c..de4b13b06 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -11,7 +11,6 @@ open Names
 open Term
 open Context
 open Termops
-open Sign
 open Environ
 open Libnames
 open Globnames
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4e63b16fa..c7f4635c9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -98,7 +98,7 @@ let global_reference id =
 
 let construct_reference ctx id =
   try
-    Term.mkVar (let _ = Sign.lookup_named id ctx in id)
+    Term.mkVar (let _ = Context.lookup_named id ctx in id)
   with Not_found ->
     global_reference id
 
@@ -636,7 +636,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
     (* Is [id] a goal or section variable *)
-    let _ = Sign.lookup_named id namedctx in
+    let _ = Context.lookup_named 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 1fa0db911..e352c7f7a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Context
-open Sign
 open Evd
 open Environ
 open Libnames
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 66be2ae5a..df29d0592 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -10,7 +10,7 @@ open Loc
 open Names
 open Decl_kinds
 open Term
-open Sign
+open Context
 open Evd
 open Environ
 open Nametab
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 } *)
 
diff --git a/library/declare.mli b/library/declare.mli
index fa9917a13..602cd64fa 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -9,7 +9,7 @@
 open Names
 open Libnames
 open Term
-open Sign
+open Context
 open Declarations
 open Entries
 open Indtypes
diff --git a/library/decls.ml b/library/decls.ml
index a93913a77..2d8807f80 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -11,7 +11,7 @@
 
 open Util
 open Names
-open Sign
+open Context
 open Decl_kinds
 open Libnames
 
diff --git a/library/decls.mli b/library/decls.mli
index 87d963cd4..001d060e8 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Sign
+open Context
 open Libnames
 open Decl_kinds
 
diff --git a/library/global.mli b/library/global.mli
index a06d4640e..6ca5bfb83 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,7 +31,7 @@ val env_is_empty : unit -> bool
 
 val universes : unit -> universes
 val named_context_val : unit -> Environ.named_context_val
-val named_context : unit -> Sign.named_context
+val named_context : unit -> Context.named_context
 
 val env_is_empty : unit -> bool
 
diff --git a/library/lib.mli b/library/lib.mli
index a37d7a113..ce57721fb 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -187,7 +187,7 @@ type variable_info = Names.Id.t * Decl_kinds.binding_kind *
 type variable_context = variable_info list
 
 val instance_from_variable_context : variable_context -> Names.Id.t array
-val named_of_variable_context : variable_context -> Sign.named_context
+val named_of_variable_context : variable_context -> Context.named_context
 
 val section_segment_of_constant : Names.constant -> variable_context
 val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context
@@ -197,8 +197,8 @@ val is_in_section : Globnames.global_reference -> bool
 
 val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> unit
 
-val add_section_constant : Names.constant -> Sign.named_context -> unit
-val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit
+val add_section_constant : Names.constant -> Context.named_context -> unit
+val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit
 val replacement_context : unit ->
   (Names.Id.t array Names.Cmap.t * Names.Id.t array Names.Mindmap.t)
 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 2b4b6245a..e98a0952b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env =
   let new_env = add_pat_variables  env pat typ in
   let res =
     fst (
-      Sign.fold_rel_context
+      Context.fold_rel_context
 	(fun (na,v,t) (env,ctxt) ->
 	 match na with
 	   | Anonymous -> assert false
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 4330948aa..b397cc3d5 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -10,7 +10,7 @@ open Pp
 open Evd
 open Names
 open Term
-open Sign
+open Context
 open Environ
 open Evarutil
 open Glob_term
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index f2f5c9eff..cb478777f 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -11,7 +11,6 @@ open Pp
 open Names
 open Term
 open Context
-open Sign
 open Environ
 open Glob_term
 open Termops
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 30495857a..9d0c79143 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -8,7 +8,7 @@
 
 open Names
 open Term
-open Sign
+open Context
 open Environ
 open Termops
 open Reductionops
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 5719d750e..14c102cbc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -62,10 +62,10 @@ let env_nf_betaiotaevar sigma env =
       push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env
 
 let nf_named_context_evar sigma ctx =
-  Sign.map_named_context (Reductionops.nf_evar sigma) ctx
+  Context.map_named_context (Reductionops.nf_evar sigma) ctx
 
 let nf_rel_context_evar sigma ctx =
-  Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
+  Context.map_rel_context (Reductionops.nf_evar sigma) ctx
 
 let nf_env_evar sigma env =
   let nc' = nf_named_context_evar sigma (Environ.named_context env) in
@@ -305,7 +305,7 @@ let push_rel_context_to_named_context env typ =
   (* with vars of the rel context *)
   (* We do keep the instances corresponding to local definition (see above) *)
   let (subst, _, env) =
-    Sign.fold_rel_context
+    Context.fold_rel_context
       (fun (na,c,t) (subst, avoid, env) ->
 	let id = next_name_away na avoid in
 	let d = (id,Option.map (substl subst) c,substl subst t) in
@@ -433,7 +433,7 @@ let rec check_and_clear_in_constr evdref err ids c =
             begin match rids with
             | [] -> c
             | _ ->
-	      let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
+	      let env = Context.fold_named_context push_named nhyps ~init:(empty_env) in
 	      let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
 	      evdref := Evd.define evk ev' !evdref;
 	      let (evk',_) = destEvar ev' in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 26d85ac94..889b2c9bf 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -12,7 +12,6 @@ open Names
 open Glob_term
 open Term
 open Context
-open Sign
 open Evd
 open Environ
 open Reductionops
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f7ec791b7..52c24a3f2 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -10,7 +10,7 @@ open Loc
 open Pp
 open Names
 open Term
-open Sign
+open Context
 open Environ
 open Libnames
 open Mod_subst
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 730332514..4e8224879 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -8,7 +8,7 @@
 
 open Pp
 open Names
-open Sign
+open Context
 open Term
 open Libnames
 open Nametab
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 038bf465a..204f506a6 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -12,7 +12,6 @@ open Context
 open Declarations
 open Environ
 open Evd
-open Sign
 
 (** The following three functions are similar to the ones defined in
    Inductive, but they expect an env *)
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 8148fe25d..4a4649cca 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -8,7 +8,7 @@
 
 open Pp
 open Names
-open Sign
+open Context
 open Term
 open Environ
 open Globnames
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 69994531d..996b75146 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -9,7 +9,7 @@
 open Pp
 open Names
 open Term
-open Sign
+open Context
 open Environ
 open Glob_term
 open Inductiveops
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 26325872f..6253fcfbf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -25,7 +25,6 @@ open Pp
 open Errors
 open Util
 open Names
-open Sign
 open Evd
 open Term
 open Vars
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index e637d2b8e..04d29ac28 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -13,7 +13,7 @@
    implicit arguments. *)
 
 open Names
-open Sign
+open Context
 open Term
 open Environ
 open Evd
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index bf4557fc2..57ae3a857 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Term
-open Sign
+open Context
 open Libnames
 open Mod_subst
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 0128f8bde..8a5a82803 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -827,9 +827,9 @@ let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d =
 
 let vars_of_env env =
   let s =
-    Sign.fold_named_context (fun (id,_,_) s -> Id.Set.add id s)
+    Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s)
       (named_context env) ~init:Id.Set.empty in
-  Sign.fold_rel_context
+  Context.fold_rel_context
     (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s)
     (rel_context env) ~init:s
 
@@ -855,12 +855,12 @@ let lookup_rel_of_name id names =
 let empty_names_context = []
 
 let ids_of_rel_context sign =
-  Sign.fold_rel_context
+  Context.fold_rel_context
     (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
     sign ~init:[]
 
 let ids_of_named_context sign =
-  Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
+  Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
 
 let ids_of_context env =
   (ids_of_rel_context (rel_context env))
@@ -997,10 +997,10 @@ let process_rel_context f env =
   let sign = named_context_val env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
-  Sign.fold_rel_context f rels ~init:env0
+  Context.fold_rel_context f rels ~init:env0
 
 let assums_of_rel_context sign =
-  Sign.fold_rel_context
+  Context.fold_rel_context
     (fun (na,c,t) l ->
       match c with
           Some _ -> l
@@ -1072,7 +1072,7 @@ let global_vars_set_of_decl env = function
 let dependency_closure env sign hyps =
   if Id.Set.is_empty hyps then [] else
     let (_,lh) =
-      Sign.fold_named_context_reverse
+      Context.fold_named_context_reverse
         (fun (hs,hl) (x,_,_ as d) ->
           if Id.Set.mem x hs then
             (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9547231af..552513a27 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -11,7 +11,6 @@ open Pp
 open Names
 open Term
 open Context
-open Sign
 open Environ
 open Locus
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 53171d02c..4dc6280f1 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -13,7 +13,6 @@ open Decl_kinds
 open Term
 open Vars
 open Context
-open Sign
 open Evd
 open Environ
 open Util
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index af6824924..46877a58f 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -11,7 +11,6 @@ open Globnames
 open Decl_kinds
 open Term
 open Context
-open Sign
 open Evd
 open Environ
 open Nametab
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index f80ff00fc..a55b9204e 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -11,7 +11,6 @@ open Names
 open Decl_kinds
 open Term
 open Context
-open Sign
 open Evd
 open Environ
 open Nametab
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 2747abe60..1bf8c6ab3 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -8,7 +8,7 @@
 
 open Pp
 open Names
-open Sign
+open Context
 open Term
 open Environ
 open Reductionops
diff --git a/printing/printer.ml b/printing/printer.ml
index 27266cfe1..5d63d179d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Term
 open Vars
-open Sign
 open Context
 open Environ
 open Globnames
@@ -245,7 +244,7 @@ let pr_named_context_of env =
   hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
 let pr_named_context env ne_context =
-  hv 0 (Sign.fold_named_context
+  hv 0 (Context.fold_named_context
 	  (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d)
           ne_context ~init:(mt ()))
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 55058ae16..fea8c0673 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -12,7 +12,6 @@ open Libnames
 open Globnames
 open Term
 open Context
-open Sign
 open Environ
 open Glob_term
 open Pattern
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 461b38a6a..bfb5ee27c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -8,7 +8,7 @@
 
 open Names
 open Term
-open Sign
+open Context
 open Environ
 open Evd
 open Evarutil
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index cf8c5dff8..dd46f1ec7 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -8,7 +8,7 @@
 
 open Names
 open Term
-open Sign
+open Context
 open Evd
 open Clenv
 open Proof_type
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 4cd3e4746..bb1c0639e 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -191,7 +191,7 @@ module V82 : sig
   val extra : Evd.evar_map -> goal -> Evd.Store.t
 
   (* Old style filtered_context primitive *)
-  val filtered_context : Evd.evar_map -> goal -> Sign.named_context
+  val filtered_context : Evd.evar_map -> goal -> Context.named_context
 
   (* Old style mk_goal primitive, returns a new goal with corresponding 
        hypotheses and conclusion, together with a term which is precisely
@@ -228,7 +228,7 @@ module V82 : sig
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
  (* Used for congruence closure *)
-  val new_goal_with : Evd.evar_map -> goal -> Sign.named_context -> goal Evd.sigma
+  val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma
 
   (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 40feb5c56..eff766b7c 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -8,7 +8,7 @@
 
 open Names
 open Term
-open Sign
+open Context
 open Evd
 open Environ
 open Proof_type
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d8609ed80..c07db32b7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -176,7 +176,7 @@ let solve_by_implicit_tactic env sigma (evk,args) =
   match (!implicit_tactic, snd (evar_source evk sigma)) with
   | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
-	Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
+	Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
       (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac)
        with e when Logic.catchable_exception e -> raise Exit)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9d22b60e0..090edde5a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -10,7 +10,7 @@ open Loc
 open Pp
 open Names
 open Term
-open Sign
+open Context
 open Environ
 open Decl_kinds
 open Tacmach
@@ -141,7 +141,7 @@ val set_end_tac : tactic -> unit
 (** [set_used_variables l] declares that section variables [l] will be
     used in the proof *)
 val set_used_variables : Id.t list -> unit
-val get_used_variables : unit -> Sign.section_context option
+val get_used_variables : unit -> Context.section_context option
 
 (** {6 ... } *)
 (** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
diff --git a/proofs/proof.ml b/proofs/proof.ml
index c38f80a55..6cc43de72 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -127,7 +127,7 @@ type proof_state = {
 
 type proof_info = {
   mutable endline_tactic : unit Proofview.tactic ;
-  mutable section_vars : Sign.section_context option;
+  mutable section_vars : Context.section_context option;
   initial_conclusions : Term.types list
 }
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 7d82ee91e..b563452a9 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -139,8 +139,8 @@ val is_last_focus : 'a focus_kind -> proof -> bool
 val no_focused_goal : proof -> bool
 
 (* Sets the section variables assumed by the proof *)
-val set_used_variables : Sign.section_context -> proof -> unit
-val get_used_variables : proof -> Sign.section_context option
+val set_used_variables : Context.section_context -> proof -> unit
+val get_used_variables : proof -> Context.section_context option
 
 (*** Endline tactic ***)
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index c1ca6a694..7fa44cf86 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -78,7 +78,7 @@ val set_endline_tactic : unit Proofview.tactic -> unit
 
 (** Sets the section variables assumed by the proof *)
 val set_used_variables : Names.Id.t list -> unit
-val get_used_variables : unit -> Sign.section_context option
+val get_used_variables : unit -> Context.section_context option
 
 (** Appends the endline tactic of the current proof to a tactic. *)
 val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 04d125804..5a71b6816 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -190,10 +190,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
    something similar (better?) in the xml protocol. *)
 let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     :Proof_type.goal list Evd.sigma =
-  let oldhyps:Sign.named_context = pf_hyps goal in
+  let oldhyps:Context.named_context = pf_hyps goal in
   let rslt:Proof_type.goal list Evd.sigma = tac goal in
   let {it=gls;sigma=sigma} = rslt in
-  let hyps:Sign.named_context list =
+  let hyps:Context.named_context list =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma}) gls in
   let newhyps =
     List.map (fun hypl -> List.subtract hypl oldhyps) hyps in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index d353a566f..c198958e3 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Term
-open Sign
+open Context
 open Evd
 open Proof_type
 open Tacexpr
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 2b5114174..813a0d850 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -51,7 +51,7 @@ let pf_last_hyp gl = List.hd (pf_hyps gl)
 
 let pf_get_hyp gls id =
   try
-    Sign.lookup_named id (pf_hyps gls)
+    Context.lookup_named id (pf_hyps gls)
   with Not_found ->
     error ("No such hypothesis: " ^ (Id.to_string id))
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 5b502f2c9..1c0ab2d14 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Context
-open Sign
 open Environ
 open Evd
 open Reduction
diff --git a/tactics/auto.mli b/tactics/auto.mli
index a93f9be26..99f4768c2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Context
-open Sign
 open Proof_type
 open Tacmach
 open Clenv
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 18e582b31..2dc42e35f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1392,7 +1392,7 @@ user = raise user error specific to rewrite
 let unfold_body x gl =
   let hyps = pf_hyps gl in
   let xval =
-    match Sign.lookup_named x hyps with
+    match Context.lookup_named x hyps with
         (_,Some xval,_) -> xval
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis.") in
@@ -1474,7 +1474,7 @@ let subst_one_var dep_proof_ok x gl =
   let (hyp,rhs,dir) =
     try
       let test hyp _ = is_eq_x gl varx hyp in
-      Sign.fold_named_context test ~init:() hyps;
+      Context.fold_named_context test ~init:() hyps;
       errorlabstrm "Subst"
         (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	 str".")
diff --git a/tactics/equality.mli b/tactics/equality.mli
index d341db4f4..aa1bfaa0f 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -11,7 +11,6 @@ open Pp
 open Names
 open Term
 open Context
-open Sign
 open Evd
 open Environ
 open Proof_type
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 1367bb87a..b38eb654b 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -8,7 +8,7 @@
 
 open Names
 open Term
-open Sign
+open Context
 open Evd
 open Pattern
 open Coqlib
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 86651e76c..ac4cd5442 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -14,7 +14,7 @@ open Term
 open Vars
 open Termops
 open Namegen
-open Sign
+open Context
 open Evd
 open Printer
 open Reductionops
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index b2d39b57a..4625cc84b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -12,7 +12,7 @@ open Util
 open Names
 open Term
 open Termops
-open Sign
+open Context
 open Declarations
 open Tacmach
 open Clenv
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3ab04dcbd..13eaaff5c 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -11,7 +11,6 @@ open Pp
 open Names
 open Term
 open Context
-open Sign
 open Tacmach
 open Proof_type
 open Clenv
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a4b89f865..21487a36d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -11,7 +11,6 @@ open Errors
 open Util
 open Names
 open Nameops
-open Sign
 open Term
 open Vars
 open Context
@@ -1552,7 +1551,7 @@ let generalize_dep ?(with_let=false) c gl =
       d::toquant
     else
       toquant in
-  let to_quantify = Sign.fold_named_context seek sign ~init:[] in
+  let to_quantify = Context.fold_named_context seek sign ~init:[] in
   let to_quantify_rev = List.rev to_quantify in
   let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
   let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
@@ -1837,7 +1836,7 @@ let assert_by na t tac = forward (Some tac) (ipat_of_name na) t
 let unfold_body x gl =
   let hyps = pf_hyps gl in
   let xval =
-    match Sign.lookup_named x hyps with
+    match Context.lookup_named x hyps with
         (_,Some xval,_) -> xval
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis.") in
@@ -2387,7 +2386,7 @@ let hyps_of_vars env sign nogen hyps =
   if Id.Set.is_empty hyps then [] 
   else
     let (_,lh) =
-      Sign.fold_named_context_reverse
+      Context.fold_named_context_reverse
         (fun (hs,hl) (x,_,_ as d) ->
 	  if Id.Set.mem x nogen then (hs,hl)
 	  else if Id.Set.mem x hs then (hs,x::hl)
@@ -3526,7 +3525,7 @@ let abstract_subproof id tac gl =
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) ->
 	if mem_named_context id current_sign &
-          interpretable_as_section_decl (Sign.lookup_named id current_sign) d
+          interpretable_as_section_decl (Context.lookup_named id current_sign) d
         then (s1,push_named_context_val d s2)
 	else (add_named_decl d s1,s2))
       global_sign (empty_named_context,empty_named_context_val) in
@@ -3562,7 +3561,7 @@ let admit_as_an_axiom gl =
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) ->
 	 if mem_named_context id current_sign &
-           interpretable_as_section_decl (Sign.lookup_named id current_sign) d
+           interpretable_as_section_decl (Context.lookup_named id current_sign) d
          then (s1,add_named_decl d s2)
 	 else (add_named_decl d s1,s2))
       global_sign (empty_named_context,empty_named_context) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f39ed97f8..2b45ecde6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -12,7 +12,6 @@ open Names
 open Term
 open Context
 open Environ
-open Sign
 open Tacmach
 open Proof_type
 open Reduction
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 1eaf6b768..b05f94c3c 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -10,7 +10,7 @@ open Term
 open Names
 open Libnames
 open Mod_subst
-open Sign
+open Context
 open Proof_type
 open Ind_tables
 
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
index fcd46c3e8..ebaaee12d 100644
--- a/toplevel/autoinstance.mli
+++ b/toplevel/autoinstance.mli
@@ -12,7 +12,6 @@ open Typeclasses
 open Names
 open Evd
 open Context
-open Sign
 
 (** {6 Automatic detection of (some) record instances } *)
 
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index d05eff126..0a71921b0 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -10,7 +10,6 @@ open Names
 open Decl_kinds
 open Term
 open Context
-open Sign
 open Evd
 open Environ
 open Nametab
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6a3d9a11a..e3a299340 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -316,10 +316,10 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env_params evd in
   let sigma = evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
-  let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
+  let ctx_params = Context.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
   List.iter (check_evars env_params Evd.empty evd) arities;
-  Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
+  Context.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
   List.iter (fun (_,ctyps,_) ->
     List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
     constructors;
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index aeb63c348..8d9e73e6d 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -9,7 +9,7 @@
 open Names
 open Errors
 open Util
-open Sign
+open Context
 open Term
 open Vars
 open Entries
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 8c64f3ed0..a74f69456 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Sign
+open Context
 open Cooking
 open Declarations
 open Entries
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b289bb9b0..dc906d281 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -14,7 +14,7 @@ open Namegen
 open Term
 open Termops
 open Indtypes
-open Sign
+open Context
 open Environ
 open Pretype_errors
 open Type_errors
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 35ceef86a..9dd25c63e 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -10,7 +10,7 @@ open Term
 open Names
 open Libnames
 open Mod_subst
-open Sign
+open Context
 open Declarations
 
 (** This module provides support for registering inductive scheme builders,
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 3779815e9..b237a4762 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -344,7 +344,7 @@ let start_proof_com kind thms hook =
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in
     let t', imps' = interp_type_evars_impls ~impls ~evdref env t in
-    Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
+    Context.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
     let ids = List.map pi1 ctx in
       (compute_proof_name (fst kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 53ee27f3b..a369bf505 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -13,7 +13,7 @@ open Declare
 *)
 
 open Term
-open Sign
+open Context
 open Vars
 open Names
 open Evd
@@ -205,7 +205,7 @@ open Environ
 let eterm_obligations env name evm fs ?status t ty = 
   (* 'Serialize' the evars *)
   let nc = Environ.named_context env in
-  let nc_len = Sign.named_context_length nc in
+  let nc_len = Context.named_context_length nc in
   let evm = Evarutil.nf_evar_map_undefined evm in
   let evl = List.rev (Evarutil.non_instantiated evm) in
   let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 331bf9ed5..018366667 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Context
-open Sign
 open Vernacexpr
 open Constrexpr
 open Impargs