diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Init/Datatypes.v | 2 | ||||
| -rw-r--r-- | theories/Init/Logic_TypeSyntax.v | 2 | ||||
| -rwxr-xr-x | theories/Init/Peano.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 03b7c06f08..65d0722c3c 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -80,8 +80,8 @@ Notation Snd := (snd ? ?). Hints Resolve pair inl inr : core v62. -(** Parsing only of things in [Datatypes.v] *) V7only[ +(** Parsing only of things in [Datatypes.v] *) Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot). Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot). Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot). diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index 21dd4ccec6..e48b150622 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -40,9 +40,9 @@ Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) V8only "'EXT2' x : t | p & q" (at level 200, x at level 80). ]. -(** Parsing only of things in [Logic_type.v] *) V7only[ +(** Parsing only of things in [Logic_type.v] *) Notation "< A > x == y" := (eq A x y) (A annot, at level 1, x at level 0, only parsing). diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index e5b516090b..41f26ffda9 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -205,8 +205,8 @@ Syntax constr | O [ O ] -> ["(0)"]. ]. -(* For parsing/printing based on scopes *) V7only [ +(* For parsing/printing based on scopes *) Module nat_scope. Infix 4 "+" plus : nat_scope. Infix 3 "*" mult : nat_scope. |