diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-23 09:26:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-23 09:26:07 +0000 |
| commit | ea4cd2f26f76194b0f02d0487dcfec36868dfa80 (patch) | |
| tree | a0dd07bface37cc3740460614b444321c48f4c81 /theories/Reals/Rsyntax.v | |
| 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/Reals/Rsyntax.v')
| -rw-r--r-- | theories/Reals/Rsyntax.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 0e9d174b7..9022e4f7e 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -195,21 +195,21 @@ Syntax constr Module R_scope. Delimiters "'R:" R_scope "'". -Infix NONA 4 "<=" Rle : R_scope. -Infix NONA 4 "<" Rlt : R_scope. -Infix NONA 4 ">=" Rge : R_scope. -(*Infix NONA 4 ">" Rgt : R_scope. (* Conflicts with "<..>Cases ... " *) *) -Infix 3 "+" Rplus : R_scope. -Infix 3 "-" Rminus : R_scope. -Infix 2 "*" Rmult : R_scope. +Infix NONA 5 "<=" Rle : R_scope. +Infix NONA 5 "<" Rlt : R_scope. +Infix NONA 5 ">=" Rge : R_scope. +(*Infix NONA 5 ">" Rgt : R_scope. (* Conflicts with "<..>Cases ... " *) *) +Infix 4 "+" Rplus : R_scope. +Infix 4 "-" Rminus : R_scope. +Infix 3 "*" Rmult : R_scope. +Infix LEFTA 3 "/" Rdiv : R_scope. Distfix 0 "- _" Ropp : R_scope. -Notation NONA 4 "x == y == z" (eqT R x y)/\(eqT R y z) (y at level 3): R_scope. -Notation NONA 4 "x <= y <= z" (Rle x y)/\(Rle y z) (y at level 3) : R_scope. -Notation NONA 4 "x <= y < z" (Rle x y)/\(Rlt y z) (y at level 3) : R_scope. -Notation NONA 4 "x < y < z" (Rlt x y)/\(Rlt y z) (y at level 3) : R_scope. -Notation NONA 4 "x < y <= z" (Rlt x y)/\(Rle y z) (y at level 3) : R_scope. -Notation NONA 4 "x <> y" ~(eqT R x y) : R_scope. -Infix LEFTA 2 "/" Rdiv : R_scope. +Notation NONA 5 "x == y == z" (eqT R x y)/\(eqT R y z) (y at level 4): R_scope. +Notation NONA 5 "x <= y <= z" (Rle x y)/\(Rle y z) (y at level 4) : R_scope. +Notation NONA 5 "x <= y < z" (Rle x y)/\(Rlt y z) (y at level 4) : R_scope. +Notation NONA 5 "x < y < z" (Rlt x y)/\(Rlt y z) (y at level 4) : R_scope. +Notation NONA 5 "x < y <= z" (Rlt x y)/\(Rle y z) (y at level 4) : R_scope. +Notation NONA 5 "x <> y" ~(eqT R x y) : R_scope. Distfix 0 "/ _" Rinv : R_scope. (* Warning: this hides sum and prod and breaks sumor symbolic notation *) |