diff options
| author | Pierre-Marie Pédrot | 2016-02-24 10:56:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-24 10:56:45 +0100 |
| commit | c6e233721f0a75029474d7dc3dc887d61e5ba84e (patch) | |
| tree | 96f23cdf57def01387e8ad7155ba5305bb3ec132 /plugins | |
| parent | 7fb5a9c518f30298a7a9332f0280c2ca0e690f18 (diff) | |
| parent | d96bf1b1ec79fa93787d23e1c42f803d74b49321 (diff) | |
Merge branch 'remove-quotations'
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 15 | ||||
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 15 |
2 files changed, 22 insertions, 8 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 |