Construct "T with (Definition|Module) id := c" generalized to

"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style).


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

6 files changed, 18 insertions, 10 deletions

diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4
index e0173d632..e1937b5f9 100644
--- a/parsing/g_module.ml4
+++ b/parsing/g_module.ml4
@@ -31,10 +31,10 @@ GEXTEND Gram
   ;
 
   with_declaration:
-    [ [ "Definition"; id = identref; ":="; c = Constr.constr ->
-          CWith_Definition (id,c)
-      | IDENT "Module"; id = identref; ":="; qid = qualid ->
-	  CWith_Module (id,qid)
+    [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.constr ->
+          CWith_Definition (fqid,c)
+      | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
+	  CWith_Module (fqid,qid)
       ] ]
   ;
   
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 10ffbecaf..2bb5b0630 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -34,7 +34,8 @@ let local_append l id = l@[id]
 
 GEXTEND Gram
   GLOBAL: bigint ident natural integer string preident ast
-    astlist qualid reference dirpath identref name base_ident var hyp;
+    astlist qualid reference dirpath identref name base_ident var
+    hyp;
 
  (* Compatibility: Prim.var is a synonym of Prim.ident *)
   var:
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
index 14fb119e4..667b5654e 100644
--- a/parsing/g_primnew.ml4
+++ b/parsing/g_primnew.ml4
@@ -49,7 +49,7 @@ let local_append l id = l@[id]
 
 if not !Options.v7 then
 GEXTEND Gram
-  GLOBAL: bigint qualid reference ne_string;
+  GLOBAL: bigint fullyqualid qualid reference ne_string;
   field:
     [ [ s = FIELD -> local_id_of_string s ] ]
   ;
@@ -58,6 +58,11 @@ GEXTEND Gram
       | id = field -> ([],id)
       ] ]
   ;
+  fullyqualid:
+    [ [ id = base_ident; (l,id')=fields -> loc,id::List.rev (id'::l)
+      | id = base_ident -> loc,[id]
+      ] ]
+  ;
   basequalid:
     [ [ id = base_ident; (l,id')=fields ->
           local_make_qualid (local_append l id) id'
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index acc691082..05f177512 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -372,10 +372,10 @@ GEXTEND Gram
       ] ]
   ;
   with_declaration:
-    [ [ "Definition"; id = identref; ":="; c = Constr.lconstr ->
-          CWith_Definition (id,c)
-      | IDENT "Module"; id = identref; ":="; qid = qualid ->
-	  CWith_Module (id,qid)
+    [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
+          CWith_Definition (fqid,c)
+      | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
+	  CWith_Module (fqid,qid)
       ] ]
   ;
   module_type:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 73e0b4cc8..cc7bb3dad 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -323,6 +323,7 @@ module Prim =
     let base_ident = Gram.Entry.create "Prim.base_ident"
 
     let qualid = Gram.Entry.create "Prim.qualid"
+    let fullyqualid = Gram.Entry.create "Prim.fullyqualid"
     let dirpath = Gram.Entry.create "Prim.dirpath"
 
     let ne_string = Gram.Entry.create "Prim.ne_string"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9963bad73..2fdb91254 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -117,6 +117,7 @@ module Prim :
     val integer : int Gram.Entry.e
     val string : string Gram.Entry.e
     val qualid : qualid located Gram.Entry.e
+    val fullyqualid : identifier list located Gram.Entry.e
     val reference : reference Gram.Entry.e
     val dirpath : dir_path Gram.Entry.e
     val ne_string : string Gram.Entry.e