diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 15:09:15 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 15:09:15 +0200 |
| commit | caf8402e4af75d85223e10cba68a6a145e050dab (patch) | |
| tree | e8c3af2139d78b7e0117fd4987b7eb3732381577 /kernel/declareops.ml | |
| parent | 0b20282c49253aea4429384467b75a5bdb1f8ba4 (diff) | |
Add a field in `constant_body` to track constant whose well-foundedness is assumed.
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 870aef1d2..068bc498a 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -132,7 +132,8 @@ let subst_const_body sub cb = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; - const_inline_code = cb.const_inline_code } + const_inline_code = cb.const_inline_code; + const_checked_guarded = cb.const_checked_guarded } (** {7 Hash-consing of constants } *) |