From f43d75830bec7ce179ca11a8eb1baf9381383bf4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 26 Aug 2005 13:11:25 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7322 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 89a319f09f..f221aa8b42 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -45,7 +45,7 @@ Ltac f_equal :=
   let des := destruct 1 || intro in
   let r := try reflexivity in 
   match goal with 
-   | |- ?f ?a = ?f' ?a' => cut (a=a'); des; r
+   | |- ?f ?a = ?f' ?a' => cut (a=a'); [des; r|r]
    | |- ?f ?a ?b = ?f' ?a' ?b' => 
       cut (b=b');[cut (a=a');[do 2 des; r|r]|r]
    | |- ?f ?a ?b ?c = ?f' ?a' ?b' ?c'=> 
-- 
cgit v1.2.3