1 files changed, 8 insertions, 13 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 27c1c3f3..dc5c17a7 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,7 +14,10 @@ open Context
    declarations. This includes global constants/axioms, mutual
    inductive definitions, modules and module types *)
 
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -76,12 +79,6 @@ type constant_body = {
     const_proj : projection_body option;
     const_inline_code : bool }
 
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
-
-type side_effect =
-  | SEsubproof of constant * constant_body * seff_env
-  | SEscheme of (inductive * constant * constant_body * seff_env) list * string
-    
 (** {6 Representation of mutual inductive types in the kernel } *)
 
 type recarg =
@@ -142,12 +139,10 @@ type one_inductive_body = {
     mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
     mind_consnrealargs : int array;
- (** Number of expected proper arguments of the constructors (w/o params)
-    (not used in the kernel) *)
+ (** Number of expected proper arguments of the constructors (w/o params) *)
 
     mind_consnrealdecls : int array;
- (** Length of the signature of the constructors (with let, w/o params)
-    (not used in the kernel) *)
+ (** Length of the signature of the constructors (with let, w/o params) *)
 
     mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
 
@@ -245,8 +240,8 @@ and module_body =
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
-    (** set of all constraints in the module  *)
-    mod_constraints : Univ.constraints;
+    (** set of all universes constraints in the module  *)
+    mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : Mod_subst.delta_resolver;
     mod_retroknowledge : Retroknowledge.action list }