Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3173 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 25 insertions, 39 deletions

diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index d51e7acbcb..71785ce702 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -25,8 +25,8 @@ with constr0 :=
          [ (pair ? ? $lc1 $lc2) ]
 .
 
-Infix 7 "+" sum.
-Infix RIGHTA 6 "*" prod.
+Infix 3 "+" sum.
+Infix RIGHTA 2 "*" prod.
 
 (** Pretty-printing of things in Datatypes.v *)
 
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 50c3df5de7..89bda61387 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -14,25 +14,25 @@ Require Specif.
 (** Parsing of things in Specif.v *)
 
 (* To accept {x:A|P}*B without parentheses *)
-Grammar constr constr6 :=
+Grammar constr constr2 :=
   sigprod [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}"
-            "*" constr6($c) ]
+            "*" constr2($c) ]
        -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ]
 
 | sig2prod [ "{" lconstr($lc) ":" lconstr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr6($c) ]
+           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr2($c) ]
        -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]
 
 | sigSprod [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}"
-         "*" constr6($c)]
+         "*" constr2($c)]
        -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ]
 
 | sigS2prod [ "{" lconstr($lc) ":" lconstr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr6($c) ]
+             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr2($c) ]
        -> [ (prod (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ].
 
 (* To factor with {A}+{B} *)
-Grammar constr constr6 :=
+Grammar constr constr2 :=
   sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
        -> [ (sig $c1 [$lc : $c1]$c2) ]
 
@@ -47,25 +47,21 @@ Grammar constr constr6 :=
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
 
-Grammar constr constr6 :=
-  sumbool [ "{" lconstr($lc) "}" "+" "{" lconstr($lc2) "}" ] -> 
-    [ (sumbool $lc $lc2) ].
+Notation 2 "{ x } + { y }" (sumbool x y).
+Notation LEFTA 3 " x + { y }" (sumor x y).
 
-Grammar constr constr7 :=
-  sumor [ constr7($c1) "+" "{" lconstr($c2) "}" ] ->
-    [ (sumor $c1 $c2) ]
-
-| sumsig [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] ->
+Grammar constr constr3 :=
+  sumsig [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] ->
     [ (sum $c (sig $c1 [$lc : $c1]$c2)) ]
 
-| sumsig2 [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1)
+| sumsig2 [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1)
            "|" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sum $c (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
 
-| sumsigS [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
+| sumsigS [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
        -> [ (sum $c (sigS $c1 [$lc : $c1]$c2)) ]
 
-| sumsigS2 [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1)
+| sumsigS2 [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1)
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sum $c (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
 .
@@ -118,19 +114,9 @@ Syntax constr
 (** Pretty-printing of [projS1] and [projS2] *)
   | projS1_imp [ (projS1 ? ? $a) ] -> ["(ProjS1 " $a:E ")"]  
   | projS2_imp [ (projS2 ? ? $a) ] -> ["(ProjS2 " $a:E ")"]
-  ;
-
-(** Pretty-printing of [sumbool] and [sumor] *)
-  level 7:
-    sumbool [ (sumbool $t1 $t2) ]
-       -> [ [<hov 0> "{" $t1:E "}" [0 1] "+" "{" $t2:L "}"] ]
-  | sumor [ (sumor $t1 $t2) ]
-       -> [ [<hov 0> $t1:E [0 1]  "+" "{" $t2:L "}"] ]
-  ;
 
 (** Pretty-printing of [except] *)
-  level 1:
-    Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ]
+  | Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ]
 
 (** Pretty-printing of [error] and [value] *)
   | Error_imp [ (error $t1) ]     -> [ [<hov 0> "Error" ] ]
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index e18cfdd76e..0e9d174b76 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -203,11 +203,11 @@ Infix 3 "+" Rplus : R_scope.
 Infix 3 "-" Rminus : R_scope.
 Infix 2 "*" Rmult : R_scope.
 Distfix 0 "- _" Ropp : R_scope.
-Notation NONA 4 "x == y == z" (eqT R x y)/\(eqT R y z) : R_scope.
-Notation NONA 4 "x <= y <= z" (Rle x y)/\(Rle y z) : R_scope.
-Notation NONA 4 "x <= y <  z" (Rle x y)/\(Rlt y z) : R_scope.
-Notation NONA 4 "x <  y <  z" (Rlt x y)/\(Rlt y z) : R_scope.
-Notation NONA 4 "x <  y <= z" (Rlt x y)/\(Rle y z) : 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.
 Distfix 0 "/ _" Rinv : R_scope.
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 8314d25a51..77930d10de 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -229,10 +229,10 @@ Infix 3 "+" Zplus : Z_scope.
 Infix 3 "-" Zminus : Z_scope.
 Infix 2 "*" Zmult : Z_scope.
 Distfix 0 "- _" Zopp : Z_scope.
-Notation NONA 4 "x <= y <= z" (Zle x y)/\(Zle y z) : Z_scope.
-Notation NONA 4 "x <= y <  z" (Zle x y)/\(Zlt y z) : Z_scope.
-Notation NONA 4 "x <  y <  z" (Zlt x y)/\(Zlt y z) : Z_scope.
-Notation NONA 4 "x <  y <= z" (Zlt x y)/\(Zle y z) : 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.
 (* Notation NONA 1 "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
 Notation NONA 1 "|| x ||" (Zabs x) : Z_scope.