diff options
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 15 | ||||
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 15 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 5 |
3 files changed, 26 insertions, 9 deletions
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index c96b4a4f4..04c62eb48 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 0a99a26b3..6b2b2bbfa 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 151949c3c..85b9d6a08 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)) |