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/romega | |
| parent | 7fb5a9c518f30298a7a9332f0280c2ca0e690f18 (diff) | |
| parent | d96bf1b1ec79fa93787d23e1c42f803d74b49321 (diff) | |
Merge branch 'remove-quotations'
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 15 |
1 files changed, 11 insertions, 4 deletions
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 |