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 8446bf50c..6e7acd3f5 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -36,7 +36,7 @@ let my_int_of_string loc s = GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident - fullyqualid qualid reference dirpath + fullyqualid qualid reference dirpath ne_lstring ne_string string pattern_ident pattern_identref by_notation smart_global; preident: [ [ s = IDENT -> s ] ] @@ -99,6 +99,9 @@ GEXTEND Gram if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s ] ] ; + ne_lstring: + [ [ s = ne_string -> (loc,s) ] ] + ; dirpath: [ [ id = ident; l = LIST0 field -> make_dirpath (l@[id]) ] ] |