Merge PR #7912: Simplify effects API

1 files changed, 10 insertions, 7 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 40873bea76..94248ad26b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -120,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
-
-type side_effect = {
-  from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff;
+(** Not used by the kernel. *)
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type side_eff = {
+  seff_constant : Constant.t;
+  seff_body : Declarations.constant_body;
+  seff_env : seff_env;
+  seff_role : side_effect_role;
 }