diff options
Diffstat (limited to 'plugins/setoid_ring')
| -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 9585826109..8dbef47fe1 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -206,7 +206,7 @@ let exec_tactic env evd n f args = let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd -let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n))) +let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))) let gen_reference n = lazy (Coqlib.lib_ref n) let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory" @@ -251,7 +251,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) [@@ocaml.warning "-3"] let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -901,7 +901,7 @@ let ftheory_to_obj : field_info -> obj = let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in + let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> |