Using UInfoInd for universes in inductive types

It stores both universe constraints and subtyping information for
blocks of inductive declarations.

At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 88584e3b3d..97c28025a4 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_polymorphic : bool; 
-  mind_entry_universes : Univ.universe_context * Univ.universe_context;
+  mind_entry_universes : Univ.universe_info_ind;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
   mind_entry_private : bool option;