diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 21:41:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:16:36 +0200 |
| commit | b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 (patch) | |
| tree | dd9e7016271fdad02452aed0f8cd469305e0780e /tactics/eqdecide.ml | |
| parent | a4bd166bd2119a5290276f0ded44f8186ba1ecee (diff) | |
Put the "generalize" tactic in the monad.
Diffstat (limited to 'tactics/eqdecide.ml')
| -rw-r--r-- | tactics/eqdecide.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 01ebaa7b7..b1d3290aa 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -64,7 +64,7 @@ let choose_noteq eqonleft = let mkBranches c1 c2 = tclTHENLIST - [Proofview.V82.tactic (generalize [c2]); + [generalize [c2]; Simple.elim c1; intros; onLastHyp Simple.case; |