diff options
| -rw-r--r-- | proofs/refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/refiner.mli | 5 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 8 |
3 files changed, 15 insertions, 8 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index e45834309e..cd592296d3 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 5dc61aa1b0..3a0faa7221 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 85e885a137..0ddcd61166 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 = |