Getting rid of the "<:tactic< ... >>" quotations.

It used to allow to represent parts of tactic AST directly in ML code. Most of
the uses were trivial, only calling a constant, except for tauto that had an
important code base written in this style. Removing this reduces the dependency
to CAMLPX and the preeminence of Ltac in ML code.

1 files changed, 4 insertions, 1 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 151949c3c6..85b9d6a08f 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -752,11 +752,14 @@ let case_eq_intros_rewrite x =
   end }
 
 let rec find_a_destructable_match t =
+  let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in
+  let cl = [cl, (None, None), None], None in
+  let dest = TacAtom (Loc.ghost, TacInductionDestruct(false, false, cl)) in
   match kind_of_term t with
     | Case (_,_,x,_) when closed0 x ->
 	if isVar x then
 	  (* TODO check there is no rel n. *)
-	  raise (Found (Tacinterp.eval_tactic(<:tactic<destruct x>>)))
+	  raise (Found (Tacinterp.eval_tactic dest))
 	else
 	  (* let _ = Pp.msgnl (Printer.pr_lconstr x)  in *)
 	  raise (Found (case_eq_intros_rewrite x))