aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/newring.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring/newring.ml')
-rw-r--r--plugins/setoid_ring/newring.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e20e78b1a..d84e62a93 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -283,7 +283,7 @@ let znew_ring_path =
let zltac s =
lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s))
-let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);;
+let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
(* Ring theory *)