From b0ef649660542ae840ea945d7ab4f1f3ae7b85cd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 28 Apr 2018 17:58:08 +0200
Subject: Split off Universes functions dealing with names.

This API is a bit strange, I expect it will change at some point.
---
 vernac/declareDef.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 12973f51be..c5e704a5e9 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,11 +14,11 @@ open Decl_kinds
 val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
 val declare_definition : Id.t -> definition_kind ->
-  Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
+  Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
     GlobRef.t Lemmas.declaration_hook -> GlobRef.t
 
 val declare_fix : ?opaque:bool -> definition_kind ->
-  Universes.universe_binders -> Entries.constant_universes_entry ->
+  UnivNames.universe_binders -> Entries.constant_universes_entry ->
   Id.t -> Safe_typing.private_constants Entries.proof_output ->
   Constr.types -> Impargs.manual_implicits ->
   GlobRef.t
-- 
cgit v1.2.3