diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index cd116ecb0..180596d8d 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -225,7 +225,7 @@ Syntax constr ]. (* For parsing/printing based on scopes *) -V7only [ +V7only[ Module Z_scope. ]. @@ -241,19 +241,19 @@ Infix NONA 5 ">" Zgt : Z_scope. Infix NONA 5 "?=" Zcompare : Z_scope. Notation "x <= y <= z" := (Zle x y)/\(Zle y z) (at level 5, y at level 4):Z_scope - V8only (at level 50, y at level 49). + V8only (at level 50, y at next level). Notation "x <= y < z" := (Zle x y)/\(Zlt y z) (at level 5, y at level 4):Z_scope - V8only (at level 50, y at level 49). + V8only (at level 50, y at next level). Notation "x < y < z" := (Zlt x y)/\(Zlt y z) (at level 5, y at level 4):Z_scope - V8only (at level 50, y at level 49). + V8only (at level 50, y at next level). Notation "x < y <= z" := (Zlt x y)/\(Zle y z) (at level 5, y at level 4):Z_scope - V8only (at level 50, y at level 49). + V8only (at level 50, y at next level). Notation "x = y = z" := x=y/\y=z (at level 5, y at level 4) : Z_scope - V8only (at level 50, y at level 49). + V8only (at level 50, y at next level). (* Now a polymorphic notation Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope. @@ -265,10 +265,9 @@ V7only[ (* Overwrite the printing of "`x = y`" *) Syntax constr level 0: Zeq [ (eq Z $n1 $n2) ] -> [[<hov 0> $n1 [1 0] "= " $n2 ]]. -]. -V7only [ Open Scope Z_scope. + End Z_scope. ]. @@ -279,4 +278,3 @@ Delimits Scope Z_scope with Z. Arguments Scope POS [positive_scope]. Arguments Scope NEG [positive_scope]. - |