From a6efb365f21eb1d3def5ab7b07efe2a817cff3c1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 19 Dec 2001 12:22:12 +0000
Subject: Tentative d'amélioration du résultat de Intuition

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

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index f8ad93280e..a26f234013 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -126,7 +126,13 @@ let compute = function
     let ast_id = nvar id in
     interp <:tactic<Compute in $ast_id>>
 
-let reduction = Tacticals.onAllClauses (fun ido -> compute ido)
+let red = function
+  | None -> interp <:tactic<Repeat Red>>
+  | Some id ->
+    let ast_id = nvar id in
+    interp <:tactic<Repeat Red in $ast_id>>
+
+let reduction = Tacticals.onAllClauses
 
 (* As a simple heuristic, first we try to avoid reduction both in tauto and
    intuition *)
@@ -136,14 +142,14 @@ let tauto g =
     (tclTHEN init_intros
       (tclORELSE
         (tclTHEN reduction_not_iff (interp (tacticIn tauto_main)))
-        (tclTHEN reduction (interp (tacticIn tauto_main))))) g
+        (tclTHEN (reduction compute) (interp (tacticIn tauto_main))))) g
   with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >]
 
 let intuition =
   tclTHEN init_intros
     (tclORELSE
       (tclTHEN reduction_not_iff (interp (tacticIn intuition_main)))
-      (tclTHEN reduction (interp (tacticIn intuition_main))))
+      (tclTHEN (reduction red) (interp (tacticIn intuition_main))))
 
 let _ = hide_atomic_tactic "Tauto" tauto
 let _ = hide_atomic_tactic "Intuition" intuition
-- 
cgit v1.2.3