diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-23 18:50:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-24 10:21:49 +0100 |
| commit | 60f6d46c6e623a39fc66a21cbac5aaecdf4c67c6 (patch) | |
| tree | 3f8f5508672a1b5ce62975ba81673d7fc2c7f6da /plugins/omega | |
| parent | 7fb5a9c518f30298a7a9332f0280c2ca0e690f18 (diff) | |
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.
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 15 |
1 files changed, 11 insertions, 4 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 |