diff options
| author | Gaëtan Gilbert | 2020-04-06 14:41:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-16 23:10:03 +0200 |
| commit | 3231196c77c0641d7c59191bf691378b334afc46 (patch) | |
| tree | aa10bcb9d93072e4808e831d4e4a73f88ad47349 /checker | |
| parent | 988e195c2cd0d97b664193bf1c83c3da2b380f7c (diff) | |
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checkFlags.ml | 1 | ||||
| -rw-r--r-- | checker/values.ml | 5 |
2 files changed, 5 insertions, 1 deletions
diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml index e8c7dfdfeb..1f5e76bd83 100644 --- a/checker/checkFlags.ml +++ b/checker/checkFlags.ml @@ -17,6 +17,7 @@ let set_local_flags flags env = check_positive = flags.check_positive; check_universes = flags.check_universes; conv_oracle = flags.conv_oracle; + cumulative_sprop = flags.cumulative_sprop; } in Environ.set_typing_flags flags env diff --git a/checker/values.ml b/checker/values.ml index b9efce6948..9bd381e4a9 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -241,7 +241,10 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" + [|v_bool; v_bool; v_bool; + v_oracle; v_bool; v_bool; + v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] |