aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
authorherbelin2002-11-07 14:14:56 +0000
committerherbelin2002-11-07 14:14:56 +0000
commit10e75ab2885f8c55c3df8628db2780ffb8482f90 (patch)
tree093913ed48d2eb66b744f6c778d1dbcadf23e789 /theories
parentca90f1c666f9ab936adc5c9c3965dfd1b1d5cdf1 (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.v57
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 ' ]
-.