From b797ba85b7b0f82d66af5629ccf6f75d90dda99a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 8 May 2014 18:36:34 +0200 Subject: Avoid "revert" to retype-check the goal, and move it to a "new" tactic. --- tactics/equality.ml | 2 +- tactics/rewrite.ml | 2 +- tactics/tacinterp.ml | 5 +++-- tactics/tactics.ml | 21 +++++++++++---------- 4 files changed, 16 insertions(+), 14 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index ad54fca23..51e88a7c0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1627,7 +1627,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then - [Proofview.V82.tactic (revert dephyps); + [new_revert dephyps; general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); (tclMAP intro_using dephyps)] else diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 9dd6c941e..eb9bbb5e3 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1421,7 +1421,7 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl = let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in tclTHENLAST (Tacmach.internal_cut false name newt) - (tclTHEN (Tactics.revert [name]) (Tacmach.refine p)) + (tclTHEN (Proofview.V82.of_tactic (Tactics.new_revert [name])) (Tacmach.refine p)) | None, None -> change_in_concl None newt in tclTHEN (evartac undef) tac in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0d2b3d5a1..e838dc52d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1699,8 +1699,9 @@ and interp_atomic ist tac = gl end | TacRevert l -> - Proofview.V82.tactic begin fun gl -> - Tactics.revert (interp_hyp_list ist (pf_env gl) l) gl + Proofview.Goal.raw_enter begin fun gl -> + let env = Proofview.Goal.env gl in + Tactics.new_revert (interp_hyp_list ist env l) end (* Constructors *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index da33ecfd8..e9c65a97d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1914,6 +1914,13 @@ let bring_hyps hyps = end end +let new_revert hyps = + Proofview.Goal.raw_enter begin fun gl -> + let gl = Proofview.Goal.assume gl in + let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in + (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps)) + end + (* Compute a name for a generalization *) let generalized_name c t ids cl = function @@ -2039,13 +2046,6 @@ let revert hyps gl = hyps in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl -let new_revert hyps = - Proofview.Goal.raw_enter begin fun gl -> - let gl = Proofview.Goal.assume gl in - let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in - (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps)) - end - (* Faudra-t-il une version avec plusieurs args de generalize_dep ? Cela peut-être troublant de faire "Generalize Dependent H n" dans "n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la @@ -2783,9 +2783,10 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = in if List.is_empty vars then tac else Tacticals.New.tclTHEN tac - (Proofview.V82.tactic (fun gl -> tclFIRST [revert vars ; - tclMAP (fun id -> - tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl)) + (Tacticals.New.tclFIRST + [new_revert vars ; + Proofview.V82.tactic (fun gl -> tclMAP (fun id -> + tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) end let rec compare_upto_variables x y = -- cgit v1.2.3