diff options
| -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 |