Merging Context and Sign.

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

13 files changed, 16 insertions, 17 deletions

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