summaryrefslogtreecommitdiff
path: root/plugins/nsatz
diff options
context:
space:
mode:
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.ml2
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")