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 ef3e1bb6ae..591a7d404c 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -74,7 +74,9 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *) +} type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] |