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/obligations.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/obligations.ml') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6de8539d4..624edeffe 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -259,7 +259,7 @@ let eterm_obligations env name evm fs ?status t ty = let tactics_module = ["Program";"Tactics"] let safe_init_constant md name () = Coqlib.check_required_library ("Coq"::md); - Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name) + UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name) let hide_obligation = safe_init_constant tactics_module "obligation" let pperror cmd = CErrors.user_err ~hdr:"Program" cmd -- cgit v1.2.3