diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/omega/g_omega.mlg | 33 |
1 files changed, 1 insertions, 32 deletions
diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg index 84964a7bd2..7c653b223e 100644 --- a/plugins/omega/g_omega.mlg +++ b/plugins/omega/g_omega.mlg @@ -21,40 +21,9 @@ DECLARE PLUGIN "omega_plugin" { open Ltac_plugin -open Names -open Coq_omega -open Stdarg - -let eval_tactic name = - let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make (ModPath.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" -> eval_tactic "zify_nat" - | "positive" -> eval_tactic "zify_positive" - | "N" -> eval_tactic "zify_N" - | "Z" -> eval_tactic "zify_op" - | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s))) - (Util.List.sort_uniquize String.compare l) - in - Tacticals.New.tclTHEN - (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) - (omega_solver) } TACTIC EXTEND omega -| [ "omega" ] -> { omega_tactic [] } +| [ "omega" ] -> { Coq_omega.omega_solver } END - -TACTIC EXTEND omega' -| [ "omega" "with" ne_ident_list(l) ] -> - { omega_tactic (List.map Names.Id.to_string l) } -| [ "omega" "with" "*" ] -> - { Tacticals.New.tclTHEN (eval_tactic "zify") (omega_tactic []) } -END - |