From 1d08096be11d3b0a8aeed8e2b1d94f92bab7d965 Mon Sep 17 00:00:00 2001
From: courant
Date: Thu, 2 May 2002 11:37:28 +0000
Subject: nettoyage code

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

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 3e760e5728..eea887e727 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -109,9 +109,6 @@ let rec tauto_intuit t_reduce t_solver ist =
       $t_solver
    ) >>
 
-let tauto_main t_reduce ist =
-  tauto_intuit t_reduce <:tactic< Failtac >> ist
-
 let unfold_not_iff = function
   | None -> interp <:tactic<Unfold not iff>>
   | Some id ->
@@ -122,18 +119,18 @@ let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
 
 let t_reduction_not_iff = valueIn (VTactic reduction_not_iff)
 
+let intuition_gen tac =
+  interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
+
 let tauto g =
-  try
-        (interp (tacticIn (tauto_main t_reduction_not_iff)))
-    g
+  try intuition_gen <:tactic<Failtac>> g
   with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >]
 
-let intuition_gen tac =
-  interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
+let default_intuition_tac = <:tactic< Auto with * >>
 
 let intuition args =
   match args with
-    | [] -> intuition_gen <:tactic< Auto with * >>
+    | [] -> intuition_gen default_intuition_tac
     | [ Tac(_, t)] -> intuition_gen t
     | _ -> assert false
 
-- 
cgit v1.2.3