diff options
Diffstat (limited to 'plugins/nsatz')
-rw-r--r-- | plugins/nsatz/g_nsatz.mlg (renamed from plugins/nsatz/g_nsatz.ml4) | 6 | ||||
-rw-r--r-- | plugins/nsatz/nsatz.ml | 2 |
2 files changed, 6 insertions, 2 deletions
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.mlg index 4ac49adb..16ff512e 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Stdarg +} + DECLARE PLUGIN "nsatz_plugin" TACTIC EXTEND nsatz_compute -| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ] +| [ "nsatz_compute" constr(lt) ] -> { Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) } END diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 81b44ffa..d2d4639d 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -136,7 +136,7 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant msg path s = Universes.constr_of_global @@ +let gen_constant msg path s = UnivGen.constr_of_global @@ coq_reference msg path s let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") |