diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 6a5b0dbb20..d74c9a0d5e 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -59,7 +59,9 @@ type constant_body = { const_native_name : native_name ref; const_inline_code : bool } -type side_effect = NewConstant of constant * constant_body +type side_effect = + | SEsubproof of constant * constant_body + | SEscheme of (inductive * constant * constant_body) list * string (** {6 Representation of mutual inductive types in the kernel } *) |