From fb956e945678e0c69766c219cd7ab026925a57ea Mon Sep 17 00:00:00 2001
From: corbinea
Date: Sun, 25 Oct 2009 19:02:13 +0000
Subject: fixed bug in Czar grammar

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12415 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_decl_mode.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index e812faeaca..f37d1e758d 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -220,8 +220,8 @@ GLOBAL: proof_instr;
   intro_step:
     [[ IDENT "suppose" ; h=assume_clause -> Psuppose h
      | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
-       po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ;
-       ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] ->
+       po=OPT[ "with"; p=LIST1 hyp SEP ","-> p  ] ; 
+       ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> 
 	 Pcase (none_is_empty po,c,none_is_empty ho)
      | "let" ; v=let_vars -> Plet v
      | IDENT "take"; witnesses = LIST1 constr SEP ","  -> Ptake witnesses
-- 
cgit v1.2.3