diff options
| author | herbelin | 2002-10-23 09:26:07 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-23 09:26:07 +0000 |
| commit | ea4cd2f26f76194b0f02d0487dcfec36868dfa80 (patch) | |
| tree | a0dd07bface37cc3740460614b444321c48f4c81 /theories/ZArith | |
| parent | 8c2e66822b81c43f6d6b216fee306f6e75aeab3f (diff) | |
Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pour
compatibilité avec la surcharge dans certains développements (p.e. Utrecht/ABP)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3176 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 77930d10de..ef9647413d 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -220,20 +220,20 @@ Syntax constr Module Z_scope. Delimiters "'Z:" Z_scope "'". -Infix NONA 4 "<=" Zle : Z_scope. -Infix NONA 4 "<" Zlt : Z_scope. -Infix NONA 4 ">=" Zge : Z_scope. -(*Infix NONA 4 ">" Zgt : Z_scope. (* Conflicts with "<..>Cases ... " *) *) -Infix NONA 4 "?=" Zcompare : Z_scope. -Infix 3 "+" Zplus : Z_scope. -Infix 3 "-" Zminus : Z_scope. -Infix 2 "*" Zmult : Z_scope. +Infix 4 "+" Zplus : Z_scope. +Infix 4 "-" Zminus : Z_scope. +Infix 3 "*" Zmult : Z_scope. Distfix 0 "- _" Zopp : Z_scope. -Notation NONA 4 "x <= y <= z" (Zle x y)/\(Zle y z) (y at level 3) : Z_scope. -Notation NONA 4 "x <= y < z" (Zle x y)/\(Zlt y z) (y at level 3) : Z_scope. -Notation NONA 4 "x < y < z" (Zlt x y)/\(Zlt y z) (y at level 3) : Z_scope. -Notation NONA 4 "x < y <= z" (Zlt x y)/\(Zle y z) (y at level 3) : Z_scope. -Notation NONA 4 "x <> y" ~(eq Z x y) : Z_scope. +Infix NONA 5 "<=" Zle : Z_scope. +Infix NONA 5 "<" Zlt : Z_scope. +Infix NONA 5 ">=" Zge : Z_scope. +(*Infix NONA 5 ">" Zgt : Z_scope. (* Conflicts with "<..>Cases ... " *) *) +Infix NONA 5 "?=" Zcompare : Z_scope. +Notation NONA 5 "x <= y <= z" (Zle x y)/\(Zle y z) (y at level 4) : Z_scope. +Notation NONA 5 "x <= y < z" (Zle x y)/\(Zlt y z) (y at level 4) : Z_scope. +Notation NONA 5 "x < y < z" (Zlt x y)/\(Zlt y z) (y at level 4) : Z_scope. +Notation NONA 5 "x < y <= z" (Zlt x y)/\(Zle y z) (y at level 4) : Z_scope. +Notation NONA 5 "x <> y" ~(eq Z x y) : Z_scope. (* Notation NONA 1 "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*) Notation NONA 1 "|| x ||" (Zabs x) : Z_scope. |