From 8c2e66822b81c43f6d6b216fee306f6e75aeab3f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 23 Oct 2002 09:25:51 +0000
Subject: 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) Déplacement de ~ au niveau 5 qui est le niveau des atomes
 propositionels

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3175 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/DatatypesSyntax.v |  4 ++--
 theories/Init/LogicSyntax.v     |  2 +-
 theories/Init/PeanoSyntax.v     | 12 ++++++------
 theories/Init/SpecifSyntax.v    | 26 +++++++++++++-------------
 4 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 71785ce702..a0543c7281 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -25,8 +25,8 @@ with constr0 :=
          [ (pair ? ? $lc1 $lc2) ]
 .
 
-Infix 3 "+" sum.
-Infix RIGHTA 2 "*" prod.
+Infix 4 "+" sum.
+Infix RIGHTA 3 "*" prod.
 
 (** Pretty-printing of things in Datatypes.v *)
 
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index b9b3418eaa..fe796f9f27 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -40,7 +40,7 @@ with constr10 :=
 | ex2implicit [ "EX" ident($v) "|" constr($c1) "&" 
            constr($c2) ] -> [ (ex2 ? [$v]$c1 [$v]$c2) ].
 
-Distfix RIGHTA 2 "~ _" not.
+Distfix RIGHTA 5 "~ _" not.
 
 Infix RIGHTA 6 "/\\" and.
 
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index 3a2b63a37b..0782c71880 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -33,12 +33,12 @@ Delimiters "'N:" nat_scope "'". (* "[N", "[N:", "]]" are conflicting *)
 (* For parsing/printing based on scopes *)
 Module nat_scope.
 
-Infix 3 "+" plus : nat_scope.
-Infix 2 "*" mult : nat_scope.
-Infix NONA 4 "<=" le : nat_scope.
-Infix NONA 4 "<" lt : nat_scope.
-Infix NONA 4 ">=" ge : nat_scope.
-(* Infix 4 ">" gt : nat_scope. (* Conflicts with "<..>Cases ... " *) *)
+Infix 4 "+" plus : nat_scope.
+Infix 3 "*" mult : nat_scope.
+Infix NONA 5 "<=" le : nat_scope.
+Infix NONA 5 "<" lt : nat_scope.
+Infix NONA 5 ">=" ge : nat_scope.
+(* Infix 5 ">" gt : nat_scope. (* Conflicts with "<..>Cases ... " *) *)
 
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
 Open Scope nat_scope.
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 89bda61387..915fefd143 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 constr2 :=
+Grammar constr constr3 :=
   sigprod [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}"
-            "*" constr2($c) ]
+            "*" constr3($c) ]
        -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ]
 
 | sig2prod [ "{" lconstr($lc) ":" lconstr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr2($c) ]
+           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ]
        -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]
 
 | sigSprod [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}"
-         "*" constr2($c)]
+         "*" constr3($c)]
        -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ]
 
 | sigS2prod [ "{" lconstr($lc) ":" lconstr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr2($c) ]
+             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ]
        -> [ (prod (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ].
 
 (* To factor with {A}+{B} *)
-Grammar constr constr2 :=
+Grammar constr constr3 :=
   sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
        -> [ (sig $c1 [$lc : $c1]$c2) ]
 
@@ -47,21 +47,21 @@ Grammar constr constr2 :=
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
 
-Notation 2 "{ x } + { y }" (sumbool x y).
-Notation LEFTA 3 " x + { y }" (sumor x y).
+Notation 3 "{ x } + { y }" (sumbool x y).
+Notation LEFTA 4 " x + { y }" (sumor x y).
 
-Grammar constr constr3 :=
-  sumsig [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] ->
+Grammar constr lassoc_constr4 :=
+  sumsig [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] ->
     [ (sum $c (sig $c1 [$lc : $c1]$c2)) ]
 
-| sumsig2 [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1)
+| sumsig2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1)
            "|" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sum $c (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
 
-| sumsigS [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
+| sumsigS [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
        -> [ (sum $c (sigS $c1 [$lc : $c1]$c2)) ]
 
-| sumsigS2 [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1)
+| sumsigS2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1)
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sum $c (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
 .
-- 
cgit v1.2.3