aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/coretactics.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/coretactics.ml4')
-rw-r--r--ltac/coretactics.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 98b77ab35..3849a8440 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -39,7 +39,7 @@ TACTIC EXTEND cut
END
TACTIC EXTEND exact_no_check
- [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ]
+ [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
END
TACTIC EXTEND vm_cast_no_check