diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-07 14:14:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-07 14:14:56 +0000 |
| commit | 10e75ab2885f8c55c3df8628db2780ffb8482f90 (patch) | |
| tree | 093913ed48d2eb66b744f6c778d1dbcadf23e789 /parsing/g_cases.ml4 | |
| 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 'parsing/g_cases.ml4')
| -rw-r--r-- | parsing/g_cases.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4 index 6bee39b12..e84a89092 100644 --- a/parsing/g_cases.ml4 +++ b/parsing/g_cases.ml4 @@ -18,6 +18,10 @@ GEXTEND Gram pattern: [ [ qid = global -> qid + (* Hack to parse syntax "(n)" as a natural number *) + | "("; G_constr.test_int_rparen; n = INT; ")" -> + let n = Coqast.Str (loc,n) in + <:ast< (PATTDELIMITERS "nat_scope" (PATTNUMERAL $n)) >> | "("; p = compound_pattern; ")" -> p | n = INT -> let n = Coqast.Str (loc,n) in <:ast< (PATTNUMERAL $n) >> |