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, 3 insertions, 2 deletions

diff --git a/API/API.mli b/API/API.mli
index e2c43dab82..cea879ba3c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -86,6 +86,8 @@ sig
   type universe_context = UContext.t
   [@@ocaml.deprecated "alias of API.Names.UContext.t"]
 
+  type universe_info_ind = Univ.UInfoInd.t
+
   module LSet : module type of struct include Univ.LSet end
   module ContextSet : 
   sig
@@ -1093,8 +1095,7 @@ sig
         mind_nparams_rec : int;
         mind_params_ctxt : Context.Rel.t;
         mind_polymorphic : bool;
-        mind_universes : Univ.UContext.t;
-        mind_subtyping : Univ.universe_context;
+        mind_universes : Univ.universe_info_ind;
         mind_private : bool option;
         mind_typing_flags : Declarations.typing_flags;
       }