From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 vernac/record.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'vernac/record.mli')

diff --git a/vernac/record.mli b/vernac/record.mli
index c43d833b0..aa530fd61 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,9 +26,7 @@ val declare_projections :
 
 val declare_structure :
   Decl_kinds.recursivity_kind ->
-  Decl_kinds.cumulative_inductive_flag ->
-  Decl_kinds.polymorphic ->
-  Univ.universe_info_ind (** universe and subtyping constraints *) ->
+  Entries.inductive_universes ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
-- 
cgit v1.2.3