Merging Context and Sign.

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

18 files changed, 19 insertions, 27 deletions

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