Imported Upstream version 8.6upstream/8.6

1 files changed, 11 insertions, 5 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index b2a77dd9..ea7c266b 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -18,8 +18,8 @@ open Term
 (** {6 Local entries } *)
 
 type local_entry =
-  | LocalDef of constr
-  | LocalAssum of constr
+  | LocalDefEntry of constr
+  | LocalAssumEntry of constr
 
 
 (** {6 Declaration of inductive types. } *)
@@ -51,7 +51,8 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list;
   mind_entry_polymorphic : bool; 
   mind_entry_universes : Univ.universe_context;
-  mind_entry_private : bool option }
+  mind_entry_private : bool option;
+}
 
 (** {6 Constants (Definition/Axiom) } *)
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
@@ -97,14 +98,19 @@ type module_entry =
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
 
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type seff_env =
+  [ `Nothing
+  (* The proof term and its universes.
+     Same as the constant_body's but not in an ephemeron *)
+  | `Opaque of Constr.t * Univ.universe_context_set ]
 
 type side_eff =
   | SEsubproof of constant * Declarations.constant_body * seff_env
   | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
 
 type side_effect = {
-  from_env : Declarations.structure_body Ephemeron.key;
+  from_env : Declarations.structure_body CEphemeron.key;
   eff      : side_eff;
 }