From a51dda2344679dc6d9145f3f34acad29721f6c75 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 19:26:21 +0200 Subject: Split off Universes functions dealing with generating new universes. --- plugins/omega/coq_omega.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/omega') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 51cd665f6..e455ebb28 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -206,7 +206,7 @@ let coq_modules = init_modules @arith_modules @ [logic_dir] @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] -let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s) +let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s) let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules -- cgit v1.2.3