From 4cc6bd53bca5441c9960ba55818b5ddfa8c8d13b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 10 Apr 2009 15:04:07 +0000
Subject: Fix tauto no longer failing after commit 12077; appropriate error
 message in the classical case.

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

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 0e14c471ad..099d60c090 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -255,14 +255,18 @@ let coq_nnpp_path =
   let dir = List.map id_of_string ["Classical_Prop";"Logic";"Coq"] in
   Libnames.make_path (make_dirpath dir) (id_of_string "NNPP")
 
-let tauto_classical g =
+let tauto_classical nnpp g =
+  try tclTHEN (apply nnpp) tauto_intuitionistic g
+  with UserError _ -> errorlabstrm "tauto" (str "Classical tauto failed.")
+
+let tauto g =
   try 
     let nnpp = constr_of_global (Nametab.absolute_reference coq_nnpp_path) in
-    tclTHEN (apply nnpp) tauto_intuitionistic g
+    (* try intuitionistic version first to avoid an axiom if possible *)
+    tclORELSE tauto_intuitionistic (tauto_classical nnpp) g
   with Not_found ->
-    tclIDTAC g
+    tauto_intuitionistic g
 
-let tauto = tclORELSE tauto_intuitionistic tauto_classical
 
 let default_intuition_tac = <:tactic< auto with * >>
 
-- 
cgit v1.2.3