From dd12efa082dcf75ddb3a7cb856b0d7785bfa6ce7 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 17 Jul 2002 14:01:46 +0000
Subject: Nettoyage de code pour la règle  [id:(?1-> ?2)-> ?3|- ?]

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

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index e327e4aace..a54b693608 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -98,8 +98,11 @@ let rec tauto_intuit t_reduce t_solver ist =
     Orelse
       (Match Reverse 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; (Assumption Orelse (Intro; Assumption))]; Solve [ $t_tauto_intuit ]
+	  Cut ?3;
+	    [Intro;Clear id
+	    |Cut ?1 -> ?2;
+	       [Exact id|Generalize [y:?2](id [x:?1]y);Intro;Clear id]
+	    ]; Solve [ $t_tauto_intuit ]
       | [|- (?1 ? ?)] ->
         $t_is_disj;Solve [Left;$t_tauto_intuit | Right;$t_tauto_intuit]
       )
-- 
cgit v1.2.3