From 8576c98510a9ea35d3145dddc19315fa3a7b9e0b Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 14 Jan 2004 14:59:49 +0000
Subject: make sure the parser for FORMULA does not require them to be enclosed
 in parentheses and parse to the end of input

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5203 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/parse.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index b46d15c4b4..3becfa29eb 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -279,7 +279,8 @@ let parse_string_action reqid phylum char_stream string_list =
       | "FORMULA" ->
        P_f
         (xlate_formula
-	   (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream)))
+	   (Gram.Entry.parse 
+              (Pcoq.eoi_entry Pcoq.Constr.lconstr) (Gram.parsable char_stream)))
       | "ID" -> P_id (CT_ident
                         (Libnames.string_of_qualid 
 			 (snd 
-- 
cgit v1.2.3