diff options
| author | corbinea | 2009-10-25 19:02:13 +0000 |
|---|---|---|
| committer | corbinea | 2009-10-25 19:02:13 +0000 |
| commit | fb956e945678e0c69766c219cd7ab026925a57ea (patch) | |
| tree | 127e7cf33856d4c8ee80bcf0ab237fbc404ae25b | |
| parent | b050bc27442c234eafcb8ad634c33897d92c2f15 (diff) | |
fixed bug in Czar grammar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12415 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_decl_mode.ml4 | 4 |
1 files 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 |