From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 1 Jul 2010 17:21:14 +0200
Subject: Imported Upstream version 8.2pl2+dfsg

---
 parsing/g_decl_mode.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing/g_decl_mode.ml4')

diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 61c3474d..35fc064b 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: g_decl_mode.ml4 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: g_decl_mode.ml4 12414 2009-10-25 18:50:41Z corbinea $ *)
 
 
 open Decl_expr
@@ -220,7 +220,7 @@ 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 ] ; 
+       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	 
-- 
cgit v1.2.3