From 3e317792aa9683e093465ce98f839c14f5c94867 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 31 Oct 2006 09:41:02 +0000
Subject: syntaxe du let in encore

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

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 33268f29c1..31e5ff906c 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -49,8 +49,8 @@ GEXTEND Gram
     [ "5" RIGHTA
       [ te = binder_tactic -> te ]
     | "4" LEFTA
-      [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
-      | ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
+      [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
+      | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
       | ta = tactic_expr; ";"; 
 	"["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
 	  let lta = List.map (function None -> TacId [] | Some t -> t) lta in 
@@ -66,8 +66,8 @@ GEXTEND Gram
           TacAbstract (tc,Some s) ]
 (*End of To do*)
     | "2" RIGHTA
-      [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1)
-      | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) ]
+      [ ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
+      | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
     | "1" RIGHTA
       [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
           TacMatchContext (b,false,mrl)
-- 
cgit v1.2.3