diff options
| author | Arnaud Spiwack | 2016-06-07 09:52:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2016-06-14 20:01:37 +0200 |
| commit | d4f3a1a807d474050a4e91e16ff7813f1db7f537 (patch) | |
| tree | 68c91e818fd7d35789c514b3db06f77ed54b8968 /kernel/declarations.mli | |
| parent | 64e94267cb80adc1b4df782cc83a579ee521b59b (diff) | |
Assume totality: dedicated type rather than bool
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
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 591a7d404c..0c085df39e 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 ] |