1 files changed, 15 insertions, 17 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 94da00c7..94248ad2 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -49,9 +49,9 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
-  mind_entry_record : (Id.t option) option; 
-  (** Some (Some id): primitive record with id the binder name of the record
-      in projections.
+  mind_entry_record : (Id.t array option) option;
+  (** Some (Some ids): primitive records with ids the binder name of each
+      record in their respective projections. Not used by the kernel.
       Some None: non-primitive record *)
   mind_entry_finite : Declarations.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
@@ -75,7 +75,7 @@ type 'a in_constant_universes_entry = 'a * constant_universes_entry
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
-  const_entry_secctx : Context.Named.t option;
+  const_entry_secctx : Constr.named_context option;
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
@@ -85,7 +85,7 @@ type 'a definition_entry = {
 
 type section_def_entry = {
   secdef_body : constr;
-  secdef_secctx : Context.Named.t option;
+  secdef_secctx : Constr.named_context option;
   secdef_feedback : Stateid.t option;
   secdef_type : types option;
 }
@@ -93,16 +93,11 @@ type section_def_entry = {
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
-    Context.Named.t option * types in_constant_universes_entry * inline
-
-type projection_entry = {
-  proj_entry_ind : MutInd.t;
-  proj_entry_arg : int }
+    Constr.named_context option * types in_constant_universes_entry * inline
 
 type 'a constant_entry =
   | DefinitionEntry of 'a definition_entry
   | ParameterEntry of parameter_entry
-  | ProjectionEntry of projection_entry
 
 (** {6 Modules } *)
 
@@ -125,11 +120,14 @@ type seff_env =
      Same as the constant_body's but not in an ephemeron *)
   | `Opaque of Constr.t * Univ.ContextSet.t ]
 
-type side_eff =
-  | SEsubproof of Constant.t * Declarations.constant_body * seff_env
-  | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string
+(** Not used by the kernel. *)
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
 
-type side_effect = {
-  from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff;
+type side_eff = {
+  seff_constant : Constant.t;
+  seff_body : Declarations.constant_body;
+  seff_env : seff_env;
+  seff_role : side_effect_role;
 }