From f33fc85b1dd2f4994dc85b0943fe503ace2cc5ff Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Dec 2015 17:47:01 +0100
Subject: Removing the last quoted auto tactic in Tauto.

---
 tactics/tauto.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 3aa9d6d793..d84f471163 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -393,7 +393,9 @@ let tauto_gen flags =
       tauto_intuitionistic flags
     end
 
-let default_intuition_tac = <:tactic< auto with * >>
+let default_intuition_tac =
+  let tac _ _ = Auto.h_auto None [] None in
+  register_tauto_tactic tac "auto_with"
 
 (* This is the uniform mode dealing with ->, not, iff and types isomorphic to
    /\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types.
-- 
cgit v1.2.3