Further cleaning of the side-effect API.

We remove internal functions and types from the API.

1 files changed, 1 insertions, 5 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 493550e5e5..53284e0e9a 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -120,6 +120,7 @@ type seff_env =
      Same as the constant_body's but not in an ephemeron *)
   | `Opaque of Constr.t * Univ.ContextSet.t ]
 
+(** Not used by the kernel. *)
 type side_effect_role =
   | Subproof
   | Schema of inductive * string
@@ -130,8 +131,3 @@ type side_eff = {
   seff_env : seff_env;
   seff_role : side_effect_role;
 }
-
-type side_effect = {
-  from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff list;
-}