diff options
| author | Pierre-Marie Pédrot | 2016-05-16 21:41:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 22:16:36 +0200 |
| commit | b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 (patch) | |
| tree | dd9e7016271fdad02452aed0f8cd469305e0780e /ltac | |
| parent | a4bd166bd2119a5290276f0ded44f8186ba1ecee (diff) | |
Put the "generalize" tactic in the monad.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 1f3eb13355..e03cc675e7 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -728,7 +728,7 @@ let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST - [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); + [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5aff262aa5..7ec1b2ca0c 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacGeneralize cl) - (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma + (Tactics.generalize_gen cl)) sigma end } | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> |