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/declareops.ml | |
| 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/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 068bc498a0..98d2877373 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -133,7 +133,7 @@ let subst_const_body sub cb = const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code; - const_checked_guarded = cb.const_checked_guarded } + const_typing_flags = cb.const_typing_flags } (** {7 Hash-consing of constants } *) |