From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 vernac/declareDef.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1e3644c371..e455b59ab2 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -19,7 +19,7 @@ val declare_definition : Id.t -> definition_kind ->
   GlobRef.t
 
 val declare_fix : ?opaque:bool -> definition_kind ->
-  UnivNames.universe_binders -> Entries.constant_universes_entry ->
+  UnivNames.universe_binders -> Entries.universes_entry ->
   Id.t -> Safe_typing.private_constants Entries.proof_output ->
   Constr.types -> Impargs.manual_implicits ->
   GlobRef.t
-- 
cgit v1.2.3