From c6a16e8cc607f70f519f3ebbd5856b8ff501d782 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 22:18:12 +0200 Subject: Put the "generalize dependent" tactic in the monad. --- ltac/coretactics.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 766f0714d..b7fc63cd5 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -261,7 +261,7 @@ END (* Generalize dependent *) TACTIC EXTEND generalize_dependent - [ "generalize" "dependent" constr(c) ] -> [ Proofview.V82.tactic (Tactics.generalize_dep c) ] + [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ] END (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) -- cgit v1.2.3