From 17f3e00d66b30a45e902bd39ace9486b3c13b2eb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 23 Jan 2006 19:11:11 +0000
Subject: Oubli lors suppression traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7922 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_prim.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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 ] ]
   ;
-- 
cgit v1.2.3