diff options
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r-- | plugins/setoid_ring/newring.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index d84e62a93..0cb72cc3a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -229,7 +229,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) @@ -274,7 +274,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) |