diff options
| -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 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)) ] . |