Share the role type between the implementations of side-effects.

We simply exploit a type isomorphism to remove the use of dedicated algebraic
types in the kernel which are actually not necessary.

1 files changed, 11 insertions, 4 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 724ed9ec7d..493550e5e5 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -120,11 +120,18 @@ 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_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;
+}
 
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff;
+  eff      : side_eff list;
 }