Restruration autour de qualidarg

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

3 files changed, 18 insertions, 7 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index e5ed92ea2f..bb6abb70bd 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -10,14 +10,21 @@ open Vernac
 
 GEXTEND Gram
   GLOBAL: identarg ne_identarg_list numarg ne_numarg_list numarg_list
-          stringarg ne_stringarg_list constrarg sortarg tacarg;
+          stringarg ne_stringarg_list constrarg sortarg tacarg 
+          qualidarg qualidconstarg;
 
   identarg:
-    [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ]
+    [ [ id = Constr.ident -> id ] ]
   ;
   ne_identarg_list:
     [ [ l = LIST1 identarg -> l ] ]
   ;
+  qualidarg:
+    [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >> ] ]
+  ;
+  qualidconstarg:
+    [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST l)) >> ] ]
+  ;
   numarg:
     [ [ n = Prim.number -> n 
        |  "-"; n = Prim.number -> Num (loc, ( - Ast.num_of_ast n)) ] ]
@@ -81,7 +88,7 @@ GEXTEND Gram
 	  <:ast< (LocateFile $f) >>
       | IDENT "Locate"; IDENT "Library"; id = identarg; "." ->
 	  <:ast< (LocateLibrary $id) >>
-      | IDENT "Locate"; id = Tactic.qualidarg; "." ->
+      | IDENT "Locate"; id = qualidarg; "." ->
 	  <:ast< (Locate $id) >>
 
        (* For compatibility (now turned into a table) *)
@@ -94,8 +101,8 @@ GEXTEND Gram
       | IDENT "Print"; "Proof"; id = identarg; "." ->
           <:ast< (PrintOpaqueId $id) >>
 (* Pris en compte dans PrintOption ci-dessous (CADUC) *)
-      | IDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >>
-      | IDENT "Search"; id = Tactic.qualidarg; "." -> <:ast< (SEARCH $id) >>
+      | IDENT "Print"; id = qualidarg; "." -> <:ast< (PrintId $id) >>
+      | IDENT "Search"; id = qualidarg; "." -> <:ast< (SEARCH $id) >>
       | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
       | IDENT "SearchPattern"; c = constrarg; l = in_or_out_modules; "." ->
 	  <:ast< (SearchPattern $c ($LIST $l)) >>
@@ -218,9 +225,9 @@ GEXTEND Gram
 
      (* Faudrait une version de qualidarg dans Prim pour respecter l'ordre *)
      | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
-       p = Tactic.qualidarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
+       p = qualidarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
      | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string;
-       p = Tactic.qualidarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >>
+       p = qualidarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >>
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
   ] ]
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 5442fd4f0a..ef838863f5 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -347,6 +347,8 @@ module Vernac =
     
     let identarg = gec "identarg"
     let ne_identarg_list = gec_list "ne_identarg_list"
+    let qualidarg = gec "qualidarg"
+    let qualidconstarg = gec "qualidconstarg"
     let numarg = gec "numarg"
     let numarg_list = gec_list "numarg_list"
     let ne_numarg_list = gec_list "ne_numarg_list"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 32b5541ad4..6cd8403987 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -159,6 +159,8 @@ module Vernac :
   sig
     val identarg : Coqast.t Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
+    val qualidarg : Coqast.t Gram.Entry.e
+    val qualidconstarg : Coqast.t Gram.Entry.e
     val numarg : Coqast.t Gram.Entry.e
     val numarg_list : Coqast.t list Gram.Entry.e
     val ne_numarg_list : Coqast.t list Gram.Entry.e