From f54f6048ca57eeae11c62907a9089d102c8d702c Mon Sep 17 00:00:00 2001
From: delahaye
Date: Mon, 5 Feb 2001 14:27:06 +0000
Subject: Message d'erreur plus explicite pour Tauto

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

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 09c7e92247..d8d3d6241c 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -12,6 +12,7 @@ open Proof_type
 open Tacmach
 open Tacinterp
 open Tactics
+open Util
 
 let is_empty () =
   if (is_empty_type (List.assoc 1 !r_lmatch)) then
@@ -91,7 +92,6 @@ let rec 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
@@ -116,17 +116,19 @@ let reduction = Tacticals.onAllClauses (fun ido -> compute ido)
 (* As a simple heuristic, first we try to avoid reduction both in *)
 (* tauto and intuition                                            *)
 
-let tauto =
-  tclTHEN (init_intros ())
-    (tclORELSE
-      (tclTHEN reduction_not_iff (interp (tauto_main ())))
-      (tclTHEN reduction (interp (tauto_main ()))))
+let tauto g =
+  try
+    (tclTHEN (init_intros ())
+      (tclORELSE
+        (tclTHEN reduction_not_iff (interp (tauto_main ())))
+        (tclTHEN reduction (interp (tauto_main ()))))) g
+  with UserError _ -> errorlabstrm "tauto" [< 'sTR "Tauto failed" >]
 
 let intuition =
- tclTHEN (init_intros ())
-  (tclORELSE
-    (tclTHEN reduction_not_iff (interp (intuition_main ())))
-    (tclTHEN reduction (interp (intuition_main ()))))
+  tclTHEN (init_intros ())
+    (tclORELSE
+      (tclTHEN reduction_not_iff (interp (intuition_main ())))
+      (tclTHEN reduction (interp (intuition_main ()))))
 
 let _ = hide_atomic_tactic "Tauto" tauto
 let _ = hide_atomic_tactic "Intuition" intuition
-- 
cgit v1.2.3