Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tacmach

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

3 files changed, 15 insertions, 8 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index e45834309..cd592296d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -28,8 +28,7 @@ let hypotheses gl = gl.evar_hyps
 let conclusion gl = gl.evar_concl
 
 let sig_it x = x.it
-let sig_sig x = x.sigma
-
+let project x = x.sigma
 
 let pf_status pf = pf.open_subgoals
 
@@ -39,6 +38,11 @@ let on_open_proofs f pf = if is_complete pf then pf else f pf
 
 let and_status = List.fold_left (+) 0
 
+(* Getting env *)
+
+let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
+let pf_hyps gls = (sig_it gls).evar_hyps
+
 (* Normalizing evars in a goal. Called by tactic Local_constraints
    (i.e. when the sigma of the proof tree changes). Detect if the
    goal is unchanged *)
@@ -898,7 +902,7 @@ let tclINFO (tac : tactic) gls =
     let pf = v (List.map leaf (sig_it sgl)) in
     let sign = (sig_it gls).evar_hyps in
     msgnl (hov 0 (str" == " ++
-                  !pp_info (sig_sig gls) sign pf))
+                  !pp_info (project gls) sign pf))
   with e when catchable_exception e -> 
     msgnl (hov 0 (str "Info failed to apply validation"))
   end;
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5dc61aa1b..3a0faa722 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -21,7 +21,10 @@ open Tacexpr
 (* The refiner (handles primitive rules and high-level tactics). *)
 
 val sig_it  : 'a sigma -> 'a
-val sig_sig : 'a sigma -> evar_map
+val project : 'a sigma -> evar_map
+
+val pf_env  : goal sigma -> Environ.env
+val pf_hyps : goal sigma -> named_context
 
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 85e885a13..0ddcd6116 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -39,10 +39,10 @@ let unpackage = Refiner.unpackage
 let repackage = Refiner.repackage
 let apply_sig_tac = Refiner.apply_sig_tac
 
-let sig_it     = Refiner.sig_it
-let project    = Refiner.sig_sig
-let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
-let pf_hyps gls = (sig_it gls).evar_hyps
+let sig_it   = Refiner.sig_it
+let project  = Refiner.project
+let pf_env   = Refiner.pf_env
+let pf_hyps  = Refiner.pf_hyps
 
 let pf_concl gls = (sig_it gls).evar_concl
 let pf_hyps_types gls  =