diff options
| author | herbelin | 2002-11-07 14:14:56 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-07 14:14:56 +0000 |
| commit | 10e75ab2885f8c55c3df8628db2780ffb8482f90 (patch) | |
| tree | 093913ed48d2eb66b744f6c778d1dbcadf23e789 /theories | |
| parent | ca90f1c666f9ab936adc5c9c3965dfd1b1d5cdf1 (diff) | |
Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' comme un entier de nat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3222 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/PeanoSyntax.v | 57 |
1 files changed, 0 insertions, 57 deletions
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v index 0782c71880..f42fccfd90 100644 --- a/theories/Init/PeanoSyntax.v +++ b/theories/Init/PeanoSyntax.v @@ -50,60 +50,3 @@ Syntax constr . End nat_scope. - -Grammar constr constr0 := - natural_nat0 [ "(" "0" ")" ] -> [ 'N: 0 ' ] -| natural_nat1 [ "(" "1" ")" ] -> [ 'N: 1 ' ] -| natural_nat2 [ "(" "2" ")" ] -> [ 'N: 2 ' ] -| natural_nat3 [ "(" "3" ")" ] -> [ 'N: 3 ' ] -| natural_nat4 [ "(" "4" ")" ] -> [ 'N: 4 ' ] -| natural_nat5 [ "(" "5" ")" ] -> [ 'N: 5 ' ] -| natural_nat6 [ "(" "6" ")" ] -> [ 'N: 6 ' ] -| natural_nat7 [ "(" "7" ")" ] -> [ 'N: 7 ' ] -| natural_nat8 [ "(" "8" ")" ] -> [ 'N: 8 ' ] -| natural_nat9 [ "(" "9" ")" ] -> [ 'N: 9 ' ] -| natural_nat10 [ "(" "10" ")" ] -> [ 'N: 10 ' ] -| natural_nat11 [ "(" "11" ")" ] -> [ 'N: 11 ' ] -| natural_nat12 [ "(" "12" ")" ] -> [ 'N: 12 ' ] -| natural_nat13 [ "(" "13" ")" ] -> [ 'N: 13 ' ] -| natural_nat14 [ "(" "14" ")" ] -> [ 'N: 14 ' ] -| natural_nat15 [ "(" "15" ")" ] -> [ 'N: 15 ' ] -| natural_nat16 [ "(" "16" ")" ] -> [ 'N: 16 ' ] -| natural_nat17 [ "(" "17" ")" ] -> [ 'N: 17 ' ] -| natural_nat18 [ "(" "18" ")" ] -> [ 'N: 18 ' ] -| natural_nat19 [ "(" "19" ")" ] -> [ 'N: 19 ' ] -| natural_nat20 [ "(" "20" ")" ] -> [ 'N: 20 ' ] -| natural_nat21 [ "(" "21" ")" ] -> [ 'N: 21 ' ] -| natural_nat22 [ "(" "22" ")" ] -> [ 'N: 22 ' ] -| natural_nat23 [ "(" "23" ")" ] -> [ 'N: 23 ' ] -| natural_nat24 [ "(" "24" ")" ] -> [ 'N: 24 ' ] -| natural_nat25 [ "(" "25" ")" ] -> [ 'N: 25 ' ] -| natural_nat26 [ "(" "26" ")" ] -> [ 'N: 26 ' ] -| natural_nat27 [ "(" "27" ")" ] -> [ 'N: 27 ' ] -| natural_nat28 [ "(" "28" ")" ] -> [ 'N: 28 ' ] -| natural_nat29 [ "(" "29" ")" ] -> [ 'N: 29 ' ] -| natural_nat30 [ "(" "30" ")" ] -> [ 'N: 30 ' ] -(* ... *) -| natural_nat48 [ "(" "48" ")" ] -> [ 'N: 48 ' ] -| natural_nat80 [ "(" "80" ")" ] -> [ 'N: 80 ' ] -| natural_nat81 [ "(" "81" ")" ] -> [ 'N: 81 ' ] -| natural_nat91 [ "(" "91" ")" ] -> [ 'N: 91 ' ] -| natural_nat95 [ "(" "95" ")" ] -> [ 'N: 95 ' ] -| natural_nat100 [ "(" "100" ")" ] -> [ 'N: 100 ' ] -| natural_nat110 [ "(" "110" ")" ] -> [ 'N: 110 ' ] -. - -Grammar constr pattern : cases_pattern := - natural_pat0 [ "(" "0" ")" ] -> [ 'N: 0 ' ] -| natural_pat1 [ "(" "1" ")" ] -> [ 'N: 1 ' ] -| natural_pat2 [ "(" "2" ")" ] -> [ 'N: 2 ' ] -| natural_pat3 [ "(" "3" ")" ] -> [ 'N: 3 ' ] -| natural_pat4 [ "(" "4" ")" ] -> [ 'N: 4 ' ] -| natural_pat5 [ "(" "5" ")" ] -> [ 'N: 5 ' ] -| natural_pat6 [ "(" "6" ")" ] -> [ 'N: 6 ' ] -| natural_pat7 [ "(" "7" ")" ] -> [ 'N: 7 ' ] -| natural_pat8 [ "(" "8" ")" ] -> [ 'N: 8 ' ] -| natural_pat9 [ "(" "9" ")" ] -> [ 'N: 9 ' ] -| natural_pat10 [ "(" "10" ")" ] -> [ 'N: 10 ' ] -| natural_pat11 [ "(" "11" ")" ] -> [ 'N: 11 ' ] -. |
