diff options
-rwxr-xr-x | theories/Arith/Arith.v | 11 | ||||
-rw-r--r-- | theories/Zarith/Zsyntax.v | 6 |
2 files changed, 9 insertions, 8 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 1912f82d0..05fa01f06 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -14,16 +14,17 @@ Axiom My_special_variable : nat -> nat. Grammar nat number :=. -Grammar command command10 := +Grammar constr constr10 := natural_nat [ nat:number($c) ] -> [$c]. -Grammar command atomic_pattern := +Grammar constr pattern := natural_pat [ nat:number($c) ] -> [$c]. Syntax constr level 0: - myspecialvariable [<<My_special_variable>>] -> ["S"]; + myspecialvariable [ My_special_variable ] -> ["S"]; + level 10: - S [<<(S $p)>>] -> [$p:"nat_printer"] -| O [<<O>>] -> [ "0" ] + S [ (S $p) ] -> [$p:"nat_printer"] +| O [ O ] -> [ "0" ] . diff --git a/theories/Zarith/Zsyntax.v b/theories/Zarith/Zsyntax.v index bdb5ca7a8..3825fd86b 100644 --- a/theories/Zarith/Zsyntax.v +++ b/theories/Zarith/Zsyntax.v @@ -49,7 +49,7 @@ with expr1 := with expr0 := expr_id [ ident($c) ] -> [$c] -| expr_com [ "[" command:command($c) "]" ] -> [$c] +| expr_com [ "[" constr:constr($c) "]" ] -> [$c] | expr_appl [ "(" application($a) ")" ] -> [$a] | expr_num [ number($s) ] -> [$s ] | expr_negnum [ "-" negnumber($n) ] -> [ $n ] @@ -61,10 +61,10 @@ with application := | appl0 [ expr($a) ] -> [$a] . -Grammar command command0 := +Grammar constr constr0 := z_in_com [ "`" znatural:formula($c) "`" ] -> [$c]. -Grammar command atomic_pattern := +Grammar constr pattern := z_in_pattern [ "`" znatural:number($c) "`" ] -> [$c]. (* The symbols "`" "`" must be printed just once at the top of the expession, |