From b5221c0c8aca9c8051fa4b4db75324afa41027fc Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 1 Jun 2001 15:35:37 +0000
Subject: Correction d'un bug du a un Intros trop violent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1777 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tauto.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 39ed28313c..ffb7f09a15 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -97,7 +97,7 @@ let rec tauto_main () =
       (Match Context With
       | [id:(?1-> ?2)-> ?3|- ?] ->
         Cut ?2-> ?3;[Intro;Cut ?1-> ?2;[Intro;Cut ?3;[Intro;Clear id|
-          Intros;Apply id;Assumption]|Clear id]|Intros;Apply id;Intros;
+          Intros;Apply id;Assumption]|Clear id]|Intros;Apply id;Intro;
           Assumption];$t_tauto_main
       | [|- (?1 ? ?)] ->
         $t_is_disj;(Left;$t_tauto_main) Orelse (Right;$t_tauto_main))
-- 
cgit v1.2.3