From 79311e8734b5970afa3db069e9452c2521713895 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 16 May 2000 16:49:27 +0000
Subject: Retrait du i pour tclTHEN_i et correction bugs Decompose

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

(limited to 'tactics/tauto.ml')

diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 2708bf01a..52b4e288c 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1864,18 +1864,14 @@ let tautoOR ti gls =
         (t_exacto := tt;
          subbuts l thyp gls)
 
-let exact_Idtac = function 
-  | 0 -> exacto (!t_exacto)
-  | _ -> tclIDTAC
-
 let tautoOR_0 gl = 
   tclORELSE
-    (tclTHEN_i (tautoOR false) exact_Idtac 0)
+    (tclTHENSI (tautoOR false) [exacto (!t_exacto)])
     tAUTOFAIL gl
 
 let intuitionOR = 
   tclTRY (tclTHEN 
-	    (tclTHEN_i (tautoOR true) exact_Idtac 0)  
+	    (tclTHENSI (tautoOR true) [exacto (!t_exacto)])
 	    default_full_auto)
 
 (*--- Mixed code Chet-Cesar ---*)
-- 
cgit v1.2.3