diff options
| -rw-r--r-- | parsing/g_prim.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index f54904fa31..73c88540c0 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -24,7 +24,7 @@ let local_make_qualid l id = make_qualid (make_dirpath l) id GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident - fullyqualid qualid reference + fullyqualid qualid reference dirpath ne_string string; preident: [ [ s = IDENT -> s ] ] @@ -74,6 +74,10 @@ GEXTEND Gram if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s ] ] ; + dirpath: + [ [ id = ident; l = LIST0 field -> + make_dirpath (l@[id]) ] ] + ; string: [ [ s = STRING -> s ] ] ; |