Merging Context and Sign.

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

9 files changed, 10 insertions, 15 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index a93f9be265..99f4768c2b 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 18e582b31e..2dc42e35f4 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 d341db4f4b..aa1bfaa0fb 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 1367bb87a3..b38eb654be 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 86651e76cf..ac4cd54423 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 b2d39b57a4..4625cc84b5 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 3ab04dcbd5..13eaaff5ca 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 a4b89f8650..21487a36dc 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 f39ed97f8d..2b45ecde63 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