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