Merge PR#613: Cumulativity for inductive types

1 files changed, 13 insertions, 2 deletions

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 6650b6b7b0..811a28aa65 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -27,6 +27,12 @@ val subst_const_body : substitution -> constant_body -> constant_body
 
 val constant_has_body : constant_body -> bool
 
+val constant_polymorphic_instance : constant_body -> universe_instance
+val constant_polymorphic_context : constant_body -> universe_context
+
+(** Is the constant polymorphic? *)
+val constant_is_polymorphic : constant_body -> bool
+
 (** Accessing const_body, forcing access to opaque proof term if needed.
     Only use this function if you know what you're doing. *)
 
@@ -66,8 +72,13 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val inductive_instance : mutual_inductive_body -> universe_instance
-val inductive_context : mutual_inductive_body -> universe_context
+val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance
+val inductive_polymorphic_context : mutual_inductive_body -> universe_context
+
+(** Is the inductive polymorphic? *)
+val inductive_is_polymorphic : mutual_inductive_body -> bool
+(** Is the inductive cumulative? *)
+val inductive_is_cumulative : mutual_inductive_body -> bool
 
 (** {6 Kernel flags} *)