From 329283f014ea415b96e4c907ddf38d83fcd6b2bc Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 30 Jan 2001 17:44:00 +0000
Subject: Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_main

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

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4546f29f7c..f181957f37 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -88,9 +88,13 @@ let rec tauto_main () =
         Cut ?2-> ?3;[Intro;Cut ?1-> ?2;[Intro;Cut ?3;[Intro;Clear id|
           Intros;Apply id;Assumption]|Clear id]|Intros;Apply id;Intros;
           Assumption];$t_tauto_main
+      | [id:?1 -> ?2 |- ?] ->
+        Cut ?1;[Intro;Cut ?2;[Clear id ; $t_tauto_main | Intro; Apply id;
+         Assumption ]| Clear id ; $t_tauto_main]
       | [|- (?1 ? ?)] ->
         $t_is_disj;(Left;$t_tauto_main) Orelse (Right;$t_tauto_main)>>
 
+
 let intuition_main () =
   let t_axioms = tacticIn axioms
   and t_simplif = tacticIn simplif in
-- 
cgit v1.2.3