From 27958fd8bf2ed0f2811011f0854d6d0af4ae4834 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 17 Oct 2002 10:21:23 +0000 Subject: Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3154 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/PeanoSyntax.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v index e45df5a16f..f0871f6f3d 100644 --- a/theories/Init/PeanoSyntax.v +++ b/theories/Init/PeanoSyntax.v @@ -64,6 +64,24 @@ Grammar constr constr0 := | 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 ' ] . Grammar constr pattern := -- cgit v1.2.3