From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 kernel/declareops.mli | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'kernel/declareops.mli')

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} *)
 
-- 
cgit v1.2.3