diff options
Diffstat (limited to 'parsing/g_prim.ml4')
| -rw-r--r-- | parsing/g_prim.ml4 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 820514b08..2db91b8f8 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -34,7 +34,7 @@ GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring - ne_string string pattern_ident pattern_identref by_notation smart_global; + ne_string string lstring pattern_ident pattern_identref by_notation smart_global; preident: [ [ s = IDENT -> s ] ] ; @@ -106,6 +106,9 @@ GEXTEND Gram string: [ [ s = STRING -> s ] ] ; + lstring: + [ [ s = string -> (!@loc, s) ] ] + ; integer: [ [ i = INT -> my_int_of_string (!@loc) i | "-"; i = INT -> - my_int_of_string (!@loc) i ] ] |