diff options
| author | bertot | 2003-03-06 07:30:36 +0000 |
|---|---|---|
| committer | bertot | 2003-03-06 07:30:36 +0000 |
| commit | 8b1e3ffdca68c46e2019b49c1c1bcbcd07cb5776 (patch) | |
| tree | 686d7bd172797854fec0e2e0732a5fb8b8d10c05 /contrib/interface | |
| parent | 4143f9de648fa618a75804f1202f6daa0a85f718 (diff) | |
Make sure that identifiers are parsed as qualified identifier and that
the whole text is considered, not only the prefix that can be considered as
an identifier.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3745 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/parse.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index b6a0ef659e..ff3d827d97 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -280,9 +280,11 @@ let parse_string_action reqid phylum char_stream string_list = P_f (xlate_formula (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream))) - | "ID" -> P_id (xlate_ident - (Gram.Entry.parse Pcoq.Prim.ident - (Gram.parsable char_stream))) + | "ID" -> P_id (CT_ident + (Libnames.string_of_qualid + (snd + (Gram.Entry.parse (Pcoq.eoi_entry Pcoq.Prim.qualid) + (Gram.parsable char_stream))))) | "STRING" -> P_s (CT_string (Gram.Entry.parse Pcoq.Prim.string |