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. --- vernac/indschemes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/indschemes.ml') diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 32885ab88..2deca1e06 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -380,7 +380,7 @@ let do_mutual_induction_scheme lnamedepindsort = match inst with | None -> let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in - let u, ctx = Universes.fresh_instance_from ctx None in + let u, ctx = UnivGen.fresh_instance_from ctx None in let evd = Evd.from_ctx (UState.of_context_set ctx) in evd, (ind,u), Some u | Some ui -> evd, (ind, ui), inst -- cgit v1.2.3