Merge PR#613: Cumulativity for inductive types

2 files changed, 27 insertions, 9 deletions

diff --git a/API/API.ml b/API/API.ml
index 2b7bbd561..515b152e4 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -138,6 +138,7 @@ module Typeclasses = Typeclasses
 module Pretype_errors = Pretype_errors
 module Notation = Notation
 module Declarations = Declarations
+module Univops = Univops
 module Declareops = Declareops
 module Globnames = Globnames
 module Environ = Environ
diff --git a/API/API.mli b/API/API.mli
index 0d7094359..2fd3f2792 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -85,7 +85,11 @@ sig
   end
 
   type universe_context = UContext.t
-  [@@ocaml.deprecated "alias of API.Names.UContext.t"]
+  [@@ocaml.deprecated "alias of API.Univ.UContext.t"]
+
+  type abstract_universe_context = Univ.AUContext.t
+  type cumulativity_info = Univ.CumulativityInfo.t
+  type abstract_cumulativity_info = Univ.ACumulativityInfo.t
 
   module LSet : module type of struct include Univ.LSet end
   module ContextSet : 
@@ -1055,12 +1059,12 @@ sig
         proj_body : Term.constr;
       }
   type typing_flags = Declarations.typing_flags
+
   type constant_body = Declarations.constant_body = {
         const_hyps : Context.Named.t;
         const_body : constant_def;
         const_type : constant_type;
         const_body_code : Cemitcodes.to_patch_substituted option;
-        const_polymorphic : bool;
         const_universes : constant_universes;
         const_proj : projection_body option;
         const_inline_code : bool;
@@ -1093,6 +1097,12 @@ sig
                        | MEident of Names.ModPath.t
                        | MEapply of module_alg_expr * Names.ModPath.t
                        | MEwith of module_alg_expr * with_declaration
+
+  type abstract_inductive_universes = Declarations.abstract_inductive_universes =
+    | Monomorphic_ind of Univ.UContext.t
+    | Polymorphic_ind of Univ.abstract_universe_context
+    | Cumulative_ind of Univ.abstract_cumulativity_info
+
   type mutual_inductive_body = Declarations.mutual_inductive_body = {
         mind_packets : one_inductive_body array;
         mind_record : Declarations.record_body option;
@@ -1102,8 +1112,7 @@ sig
         mind_nparams : int;
         mind_nparams_rec : int;
         mind_params_ctxt : Context.Rel.t;
-        mind_polymorphic : bool;
-        mind_universes : Univ.UContext.t;
+        mind_universes : Declarations.abstract_inductive_universes;
         mind_private : bool option;
         mind_typing_flags : Declarations.typing_flags;
       }
@@ -1132,6 +1141,11 @@ sig
                             | SFBmodtype of module_type_body
 end
 
+module Univops : sig
+  val universes_of_constr : Term.constr -> Univ.LSet.t
+  val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
+end
+
 module Environ :
 sig
   type env = Prelude.env
@@ -1917,6 +1931,7 @@ end
 module Decl_kinds :
 sig
   type polymorphic = bool
+  type cumulative_inductive_flag = bool
   type recursivity_kind = Decl_kinds.recursivity_kind =
     | Finite
     | CoFinite
@@ -2398,7 +2413,7 @@ sig
   | VernacExactProof of Constrexpr.constr_expr
   | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
       inline * (plident list * Constrexpr.constr_expr) with_coercion list
-  | VernacInductive of Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
@@ -2667,8 +2682,6 @@ sig
   val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set
   val unsafe_type_of_global : Globnames.global_reference -> Term.types
   val constr_of_global : Prelude.global_reference -> Term.constr
-  val universes_of_constr : Term.constr -> Univ.LSet.t
-  val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
   val new_univ_level : Names.DirPath.t -> Univ.Level.t
   val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context
   val new_sort_in_family : Sorts.family -> Sorts.t
@@ -4757,7 +4770,9 @@ sig
   type one_inductive_impls = Command.one_inductive_impls
 
   val do_mutual_inductive :
-    (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.polymorphic -> 
+    (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list ->
+    Decl_kinds.cumulative_inductive_flag -> 
+    Decl_kinds.polymorphic -> 
     Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit
 
   val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option ->
@@ -4781,7 +4796,9 @@ sig
     structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list
 
   val interp_mutual_inductive :
-    structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.polymorphic ->
+    structured_inductive_expr -> Vernacexpr.decl_notation list ->
+    Decl_kinds.cumulative_inductive_flag ->
+    Decl_kinds.polymorphic ->
     Decl_kinds.private_flag -> Decl_kinds.recursivity_kind ->
     Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list