From fd5898afa9a89ca61f87cdeca4ae982a024e4d4b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 22:24:45 +0200
Subject: Put the "specialize_eq" tactic in the monad.

---
 ltac/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index e03cc675e7..451e0987b0 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -582,7 +582,7 @@ END
     during dependent induction. For internal use. *)
 
 TACTIC EXTEND specialize_eqs
-[ "specialize_eqs" hyp(id) ] -> [ Proofview.V82.tactic (specialize_eqs id) ]
+[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ]
 END
 
 (**********************************************************************)
-- 
cgit v1.2.3