diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-23 16:49:56 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-23 16:49:56 +0000 |
| commit | 263ec91e6664a9f1f8823c791690cb5ddf43c547 (patch) | |
| tree | d3a6d5df93ccb9701cb00f1e563bcf866d40dfdf /test-suite/success/Notations.v | |
| parent | 4aa0debbae28fa5768d2ce3f9ffe82d2a015ce39 (diff) | |
Fix the test-suite by removing any Reset in the scripts
Reset and the other backtracking commands (Back, BackTo, Backtrack)
are now allowed only during interactive session, not in compiled
or loaded scripts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15087 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Notations.v')
| -rw-r--r-- | test-suite/success/Notations.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 3c34ff928..89f110593 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -17,10 +17,12 @@ Check (nat |= nat --> nat). (* Check that first non empty definition at an empty level can be of any associativity *) -Definition marker := O. +Module Type v1. Notation "x +1" := (S x) (at level 8, left associativity). -Reset marker. +End v1. +Module Type v2. Notation "x +1" := (S x) (at level 8, right associativity). +End v2. (* Check that empty levels (here 8 and 2 in pattern) are added in the right order *) |