diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-16 21:44:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-16 22:05:15 +0200 |
| commit | 16db94e6c142217a81cc78be8788137617c24de7 (patch) | |
| tree | c52543ec1759d53f3bc14ca28f789d5bae9846b5 /tactics/tactics.ml | |
| parent | 498cbad3e5e5d69d2ee771f90de45c0fe28cc494 (diff) | |
In pat/constr introduction patterns, fixing in a better way clearing problems
of temporary hypotheses than 76f27140e6e34 did.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d0724804b..ad7ff14e6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2209,6 +2209,11 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with | IntroApplyOn (f,(loc,pat)) -> let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) destopt pat in + let doclear = + if naming = NamingMustBe (loc,id) then + 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 @@ -2217,7 +2222,9 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with (Tacticals.New.tclTHENFIRST (* Skip the side conditions of the apply *) (apply_in_once false true true true naming id - (None,(sigma,(c,NoBindings))) tac_ipat) (tac ((dloc,id)::thin) None [])) + (None,(sigma,(c,NoBindings))) + (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id))) + (tac thin None [])) sigma end |