diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2016-06-07 09:52:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2016-06-14 20:01:37 +0200 |
| commit | d4f3a1a807d474050a4e91e16ff7813f1db7f537 (patch) | |
| tree | 68c91e818fd7d35789c514b3db06f77ed54b8968 /library/global.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 'library/global.ml')
| -rw-r--r-- | library/global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index 27f7f5266..ab326e37d 100644 --- a/library/global.ml +++ b/library/global.ml @@ -77,8 +77,8 @@ let globalize_with_summary fs f = let i2l = Label.of_id -let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a) -let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d) +let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a) +let push_named_def ~flags d = globalize0 (Safe_typing.push_named_def ~flags d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set c = globalize0 (Safe_typing.push_context_set c) let push_context c = globalize0 (Safe_typing.push_context c) |