diff options
Diffstat (limited to 'plugins/setoid_ring/newring.ml')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0e1225ada..38f05978d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -230,7 +230,7 @@ let stdlib_modules = ] let coq_constant c = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)) + lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)) let coq_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) @@ -275,7 +275,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -284,7 +284,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 *) |