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.

3 files changed, 26 insertions, 9 deletions

diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index c96b4a4f4a..04c62eb487 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -17,15 +17,22 @@
 
 DECLARE PLUGIN "omega_plugin"
 
+open Names
 open Coq_omega
 
+let eval_tactic name =
+  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
+  let kn = KerName.make2 (MPfile dp) (Label.make name) in
+  let tac = Tacenv.interp_ltac kn in
+  Tacinterp.eval_tactic tac
+
 let omega_tactic l =
   let tacs = List.map
     (function
-       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
-       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
-       | "N" -> Tacinterp.interp <:tactic<zify_N>>
-       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
        | s -> Errors.error ("No Omega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 0a99a26b36..6b2b2bbfaf 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,15 +10,22 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Names
 open Refl_omega
 
+let eval_tactic name =
+  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
+  let kn = KerName.make2 (MPfile dp) (Label.make name) in
+  let tac = Tacenv.interp_ltac kn in
+  Tacinterp.eval_tactic tac
+
 let romega_tactic l =
   let tacs = List.map
     (function
-       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
-       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
-       | "N" -> Tacinterp.interp <:tactic<zify_N>>
-       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
        | s -> Errors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
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))