Oubli lors suppression traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7922 85f007b7-540e-0410-9357-904b9bb8a0f7

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 ] ]
   ;