diff options
Diffstat (limited to 'ltac/coretactics.ml4')
| -rw-r--r-- | ltac/coretactics.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index efabdc4ad..8e37653f5 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -26,6 +26,10 @@ TACTIC EXTEND reflexivity [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END +TACTIC EXTEND exact + [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] +END + TACTIC EXTEND assumption [ "assumption" ] -> [ Tactics.assumption ] END |