diff options
Diffstat (limited to 'test-suite/prerequisite')
| -rw-r--r-- | test-suite/prerequisite/make_notation.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/prerequisite/make_notation.v b/test-suite/prerequisite/make_notation.v index 4a75713d1..c93d102a2 100644 --- a/test-suite/prerequisite/make_notation.v +++ b/test-suite/prerequisite/make_notation.v @@ -1,3 +1,8 @@ (* Used in Notation.v to test import of notations from files in sections *) Notation "'Z'" := O (at level 9). +Notation plus := plus. +Notation succ := S. +Notation mult := mult (only parsing). +Notation less := le (only parsing). + |