From ee455f9c243ab7c3c5783180bae402bed2117820 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 9 May 2005 12:41:33 +0000
Subject: possibilité d'écrire [foo| ] au lieu de [foo|idtac]

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

diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index b56b310bde..265675df8d 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -48,8 +48,10 @@ GEXTEND Gram
   tactic_expr:
     [ "5" LEFTA
       [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
-      | ta = tactic_expr; ";"; "["; lta = LIST0 tactic_expr SEP "|"; "]" ->
-          TacThens (ta, lta) ]
+      | ta = tactic_expr; ";"; 
+	"["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
+	  let lta = List.map (function None -> TacId "" | Some t -> t) lta in 
+	  TacThens (ta, lta) ]
     | "4"
       [ ]
     | "3" RIGHTA
-- 
cgit v1.2.3