diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 43b908e1f..5cb406ffa 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -38,7 +38,7 @@ type inline = int option type constant_def = | Undef of inline | Def of Lazyconstr.constr_substituted - | OpaqueDef of Lazyconstr.lazy_constr + | OpaqueDef of Lazyconstr.lazy_constr Future.computation (** Linking information for the native compiler. The boolean flag indicates if the term is protected by a lazy tag *) @@ -48,15 +48,19 @@ type native_name = | LinkedInteractive of string * bool | NotLinked +type constant_constraints = Univ.constraints Future.computation + type constant_body = { const_hyps : Context.section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted; - const_constraints : Univ.constraints; + const_constraints : constant_constraints; const_native_name : native_name ref; const_inline_code : bool } +type side_effect = NewConstant of constant * constant_body + (** {6 Representation of mutual inductive types in the kernel } *) type recarg = |