aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/coretactics.ml42
1 files changed, 1 insertions, 1 deletions
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.) *)