Merge remote-tracking branch 'upstream/trunk' into trunk

1 files changed, 9 insertions, 5 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 71e228b19c..21651b3e21 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -64,7 +64,9 @@ type constant_def =
   | Def of constr Mod_subst.substituted   (** or a transparent global definition *)
   | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
 
-type constant_universes = Univ.universe_context
+type constant_universes =
+  | Monomorphic_const of Univ.universe_context
+  | Polymorphic_const of Univ.abstract_universe_context
 
 (** The [typing_flags] are instructions to the type-checker which
     modify its behaviour. The typing flags used in the type-checking
@@ -83,7 +85,6 @@ type constant_body = {
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted option;
-    const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
@@ -168,6 +169,11 @@ type one_inductive_body = {
     mind_reloc_tbl :  Cbytecodes.reloc_table;
   }
 
+type abstract_inductive_universes =
+  | Monomorphic_ind of Univ.universe_context
+  | Polymorphic_ind of Univ.abstract_universe_context
+  | Cumulative_ind of Univ.abstract_cumulativity_info
+
 type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
@@ -186,9 +192,7 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : Context.Rel.t;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_polymorphic : bool; (** Is it polymorphic or not *)
-
-    mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
+    mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)