diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 591a7d404..0c085df39 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -64,6 +64,15 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) +} + (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) type constant_body = { @@ -75,7 +84,9 @@ type constant_body = { const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; - const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *) + const_typing_flags : typing_flags; (** The typing options which + were used for + type-checking. *) } type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] |