From 33fe6e61ff2f1f8184373ed8fccc403591c4605a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Feb 2016 17:13:26 +0100
Subject: Moving the Tauto tactic to proper Ltac.

This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
---
 plugins/funind/invfun.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index cdb9c5067f..6a5a5ad533 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -474,6 +474,15 @@ let generalize_dependent_of x hyp g =
 (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
        (unfolding, substituting, destructing cases \ldots)
  *)
+let tauto =
+  let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
+  let mp = ModPath.MPfile (DirPath.make dp) in
+  let kn = KerName.make2 mp (Label.make "tauto") in
+  Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
+    let body = Tacenv.interp_ltac kn in
+    Tacinterp.eval_tactic body
+  end
+
 let  rec intros_with_rewrite g =
   observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
 and intros_with_rewrite_aux : tactic =
@@ -530,7 +539,7 @@ and intros_with_rewrite_aux : tactic =
 			  ] g
 			end
 		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
-		      Proofview.V82.of_tactic Tauto.tauto g
+		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
 			Proofview.V82.of_tactic (simplest_case v);
-- 
cgit v1.2.3