diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-27 22:36:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-27 22:36:38 +0000 |
| commit | 02deea54b806b65e315399cf721056ea7aff31a7 (patch) | |
| tree | 0ee9f993175bbff9424dadd2c4850822e2194fd4 /theories | |
| parent | 7f1e3ede102a244ffcae8e6f15e999e0edbab8cb (diff) | |
Passage command -> constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@779 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -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, |