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