diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-15 12:01:20 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-15 12:01:20 +0000 |
commit | 329b01d38e790318fba221a68fab018607e2c8f5 (patch) | |
tree | 29ad2a62ee8dbd7b427d580cb767a7102093d905 /theories/ZArith | |
parent | d3c8ce6c19ffff8d53959f3f4bf41fef85172514 (diff) |
Ajout syntaxe '>'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3437 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
-rw-r--r-- | theories/ZArith/Zsyntax.v | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 8d65afb68..f05ddeb4c 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -226,15 +226,15 @@ Module Z_scope. Delimits Scope positive_scope with P. Delimits Scope Z_scope with Z. -Infix LEFTA 4 "+" Zplus : Z_scope. -Infix LEFTA 4 "-" Zminus : Z_scope. -Infix LEFTA 3 "*" Zmult : Z_scope. +Infix "+" Zplus (at level 4) : Z_scope. +Infix "-" Zminus (at level 4) : Z_scope. +Infix "*" Zmult (at level 4) : Z_scope. Distfix 0 "- _" Zopp : Z_scope. -Infix 5 "<=" Zle : Z_scope. -Infix 5 "<" Zlt : Z_scope. -Infix 5 ">=" Zge : Z_scope. -(*Infix NONA 5 ">" Zgt : Z_scope. (* Conflicts with "<..>Cases ... " *) *) -Infix 5 "?=" Zcompare : Z_scope. +Infix "<=" Zle (at level 5, no associativity) : Z_scope. +Infix "<" Zlt (at level 5, no associativity) : Z_scope. +Infix ">=" Zge (at level 5, no associativity) : Z_scope. +Infix ">" Zgt (at level 5, no associativity) : Z_scope. +Infix "?=" Zcompare (at level 5, no associativity) : Z_scope. Notation "x <= y <= z" := (Zle x y)/\(Zle y z) (at level 5, y at level 4):Z_scope. Notation "x <= y < z" := (Zle x y)/\(Zlt y z) @@ -248,7 +248,6 @@ Notation "x = y = z" := x=y/\y=z Notation "x <> y" := ~(eq Z x y) (at level 5) : Z_scope. (* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*) -Notation "|| x ||" := (Zabs x) (at level 1) : Z_scope. (* Overwrite the printing of "`x = y`" *) Syntax constr level 0: @@ -258,11 +257,13 @@ Syntax constr level 0: (* Warning: this hides sum and prod and breaks sumor symbolic notation *) Open Scope Z_scope. +(* Syntax constr level 0: | ZZero' [ ZERO ] -> [dummy:"z_printer_ZERO"] | ZPos' [ (POS $r) ] -> [$r:"z_printer_POS":9] | ZNeg' [ (NEG $r) ] -> [$r:"z_printer_NEG":9] . +*) End Z_scope. |