diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-23 15:15:20 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-23 15:15:20 +0000 |
| commit | e61909352e809df4f21ccb88c29c3547a54d8a49 (patch) | |
| tree | a0ae2c41414287a329e1829dd0fee730029567a2 /test-suite/success/ltac.v | |
| parent | 5089c8f140560dd0fdd5db719ae84bc8e773e04d (diff) | |
test-suite: Local Tactic Notation is now legal since r15731
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/ltac.v')
| -rw-r--r-- | test-suite/success/ltac.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 1edddcfd7..c4a45b031 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -298,7 +298,3 @@ evar(foo:nat). let evval := eval compute in foo in not_eq evval 1. let evval := eval compute in foo in not_eq 1 evval. Abort. - -(* Check that this returns an error and not an anomaly (see r13667) *) - -Fail Local Tactic Notation "myintro" := intro. |