Ajout diverses entrées pour les noms qualifiés

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

2 files changed, 14 insertions, 0 deletions

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2de8d52dd3..5442fd4f0a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -250,6 +250,8 @@ module Constr =
     let constr_eoi = eoi_entry constr
     let lconstr = gec "lconstr"
     let ident = gec "ident"
+    let qualid = gec_list "qualid"
+    let global = gec "global"
     let ne_ident_comma_list = gec_list "ne_ident_comma_list"
     let ne_constr_list = gec_list "ne_constr_list"
     let sort = gec "sort"
@@ -281,6 +283,8 @@ module Tactic =
     let lconstrarg_binding_list = gec_list "lconstrarg_binding_list"
     let constrarg_list = gec_list "constrarg_list"
     let identarg = gec "identarg"
+    let qualidarg = gec "qualidarg"
+    let qualidconstarg = gec "qualidconstarg"
     let input_fun = gec "input_fun"
     let lconstrarg = gec "lconstrarg"
     let let_clause = gec "let_clause"
@@ -292,6 +296,8 @@ module Tactic =
     let match_rule = gec "match_rule"
     let match_list = gec_list "match_list"
     let ne_identarg_list = gec_list "ne_identarg_list"
+    let ne_qualidarg_list = gec_list "ne_qualidarg_list"
+    let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list"
     let ne_num_list = gec_list "ne_num_list"
     let ne_pattern_list = gec_list "ne_pattern_list"
     let ne_pattern_hyp_list = gec_list "ne_pattern_hyp_list"
@@ -374,6 +380,7 @@ module Prim =
     let grammar_entry = gec "grammar_entry"
     let grammar_entry_eoi = eoi_entry grammar_entry
     let ident = gec "ident"
+    let metaident = gec "metaident"
     let number = gec "number"
     let path = gec "path"
     let string = gec "string"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d2bb4b947e..32b5541ad4 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -85,6 +85,8 @@ module Constr :
     val constr_eoi : Coqast.t Gram.Entry.e
     val lconstr : Coqast.t Gram.Entry.e
     val ident : Coqast.t Gram.Entry.e
+    val qualid : Coqast.t list Gram.Entry.e
+    val global : Coqast.t Gram.Entry.e
     val ne_ident_comma_list : Coqast.t list Gram.Entry.e
     val ne_constr_list : Coqast.t list Gram.Entry.e
     val sort : Coqast.t Gram.Entry.e
@@ -110,6 +112,8 @@ module Tactic :
     val constrarg_list : Coqast.t list Gram.Entry.e
     val fixdecl : Coqast.t list Gram.Entry.e
     val identarg : Coqast.t Gram.Entry.e
+    val qualidarg : Coqast.t Gram.Entry.e
+    val qualidconstarg : Coqast.t Gram.Entry.e
     val input_fun : Coqast.t Gram.Entry.e
     val intropattern : Coqast.t Gram.Entry.e
     val lconstrarg : Coqast.t Gram.Entry.e
@@ -122,6 +126,8 @@ module Tactic :
     val match_rule : Coqast.t Gram.Entry.e
     val match_list : Coqast.t list Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
+    val ne_qualidarg_list : Coqast.t list Gram.Entry.e
+    val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e
     val ne_num_list : Coqast.t list Gram.Entry.e
     val ne_pattern_list : Coqast.t list Gram.Entry.e
@@ -181,6 +187,7 @@ module Prim :
     val grammar_entry : Coqast.t Gram.Entry.e
     val grammar_entry_eoi : Coqast.t Gram.Entry.e
     val ident : Coqast.t Gram.Entry.e
+    val metaident : Coqast.t Gram.Entry.e
     val number : Coqast.t Gram.Entry.e
     val path : Coqast.t Gram.Entry.e
     val string : Coqast.t Gram.Entry.e