aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/prerequisite/make_notation.v
blob: 3878e396a83031939a37e5e8f8e0a8f1d1ca3c08 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(* 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).

(* Test bug 2168: ending section of some name was removing objects of the
   same name *)

Notation add2 n:=(S n).
Section add2.
End add2.