diff options
| -rw-r--r-- | tactics/tactics.ml | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d4480ec922..3e6cea5ddd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2216,19 +2216,9 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with Proofview.tclUNIT () (* apply_in_once do a replacement *) else Proofview.V82.tactic (clear [id]) in - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let env = Proofview.Goal.env gl in - let sigma,c = f env sigma in - Tacticals.New.tclWITHHOLES false - (Tacticals.New.tclTHENFIRST - (* Skip the side conditions of the apply *) - (apply_in_once false true true true naming id - (None,(sigma,(c,NoBindings))) - (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id))) - (tac thin None [])) - sigma - end + let f env sigma = let (sigma,c) = f env sigma in (sigma,(c,NoBindings)) in + apply_in_delayed_once false true true true naming id (None,(loc,f)) + (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) and prepare_intros_loc loc dft destopt = function | IntroNaming ipat -> |