From b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 16 May 2016 21:41:55 +0200
Subject: Put the "generalize" tactic in the monad.

---
 tactics/eqdecide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/eqdecide.ml')

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;
-- 
cgit v1.2.3