diff options
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 6 |
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; -} |