From 8b1e3ffdca68c46e2019b49c1c1bcbcd07cb5776 Mon Sep 17 00:00:00 2001
From: bertot
Date: Thu, 6 Mar 2003 07:30:36 +0000
Subject: 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
---
 contrib/interface/parse.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'contrib/interface/parse.ml')

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