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 4330948aae..b397cc3d5c 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 f2f5c9effe..cb478777fd 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 30495857a0..9d0c79143a 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 5719d750e1..14c102cbcd 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 26d85ac947..889b2c9bfd 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 f7ec791b7c..52c24a3f20 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 7303325148..4e8224879c 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 038bf465a7..204f506a63 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 8148fe25dc..4a4649cca8 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 69994531d3..996b751465 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 26325872fa..6253fcfbfb 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 e637d2b8ed..04d29ac28d 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 bf4557fc27..57ae3a8579 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 0128f8bde1..8a5a828032 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 9547231afb..552513a27e 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 53171d02cb..4dc6280f12 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 af6824924f..46877a58ff 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 f80ff00fce..a55b9204ef 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