diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-23 09:25:51 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-23 09:25:51 +0000 |
commit | 8c2e66822b81c43f6d6b216fee306f6e75aeab3f (patch) | |
tree | 009f93d6143c157213ddcdd9719e86f8014776d8 | |
parent | 8d0f0114a3f2b6e352bceefcefd9b976cc4c3091 (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)
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
-rw-r--r-- | theories/Init/DatatypesSyntax.v | 4 | ||||
-rw-r--r-- | theories/Init/LogicSyntax.v | 2 | ||||
-rw-r--r-- | theories/Init/PeanoSyntax.v | 12 | ||||
-rw-r--r-- | 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 71785ce70..a0543c728 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 b9b3418ea..fe796f9f2 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 3a2b63a37..0782c7188 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 89bda6138..915fefd14 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)) ] . |