From 164a41be04b59f0191515695d731bfa1a60ba380 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 May 2000 19:35:44 +0000
Subject: Bug stupide d'ordre d'évaluation

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

diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 23b939b3cd..0130566b45 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1866,12 +1866,12 @@ let tautoOR ti gls =
 
 let tautoOR_0 gl = 
   tclORELSE
-    (tclTHENSI (tautoOR false) [exacto (!t_exacto)])
+    (tclTHENSI (tautoOR false) [fun gl -> exacto (!t_exacto) gl])
     tAUTOFAIL gl
 
 let intuitionOR = 
   tclTRY (tclTHEN 
-	    (tclTHENSI (tautoOR true) [exacto (!t_exacto)])
+	    (tclTHENSI (tautoOR true) [fun gl -> exacto (!t_exacto) gl])
 	    default_full_auto)
 
 (*--- Mixed code Chet-Cesar ---*)
@@ -1885,7 +1885,7 @@ let rec prove  tauto_intu g   =
 			    (prove tauto_intu)))
   (tclORELSE (tryAllHyps (clauseTacThen
                           (compose dyck_and_elim out_some) (prove tauto_intu)))
-  (tclORELSE (tryAllHyps (flush stdout;clauseTacThen
+  (tclORELSE (tryAllHyps (clauseTacThen
                           (compose dyck_atomic_imply_elim out_some)
                           (prove tauto_intu)))
   (tclORELSE (tryAllHyps (clauseTacThen
@@ -1896,7 +1896,7 @@ let rec prove  tauto_intu g   =
 			    (prove tauto_intu)))
   (tclORELSE (tclTHEN dyck_and_intro (prove tauto_intu))
   (tclORELSE (tclTHEN dyck_imply_intro (prove tauto_intu))
-  (tclORELSE (tryAllHyps (flush stdout;clauseTacThen
+  (tclORELSE (tryAllHyps (clauseTacThen
                           (compose dyck_or_elim out_some) (prove tauto_intu)))
   (tclORELSE (tryAllHyps (clauseTacThen (* 28/5/99, ajout par HH *)
 			    (compose dyck_imply_imply_elim out_some)
-- 
cgit v1.2.3