diff options
| author | Pierre-Marie Pédrot | 2018-03-27 16:16:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 13:50:10 +0200 |
| commit | de20a45db5d45154819f2ed4359effdbb8bf0292 (patch) | |
| tree | 4df0add753c3464868f3bc61350cdd9ff7dc445a /checker | |
| parent | 09c76adaff7adaada1c49479dfa9a4d0a4b416af (diff) | |
Turn the kernel reduction sharing flag into an argument passed in the cache.
We move the global declaration of that argument to the environment, and reuse
the Global module to handle this flag.
Note that the checker was not using this flag before this patch, and still
doesn't use it. This should probably be fixed in a later patch.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/cic.mli | 1 | ||||
| -rw-r--r-- | checker/values.ml | 4 |
2 files changed, 3 insertions, 2 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index df747692a4..17259bb438 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -220,6 +220,7 @@ type typing_flags = { points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) conv_oracle : oracle; (** Unfolding strategies for conversion *) + share_reduction : bool; (** Use by-need reduction algorithm *) } type constant_body = { diff --git a/checker/values.ml b/checker/values.ml index e68cd18b87..e1b5a949ac 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 064cd8d9651d37aebf77fb638b889cad checker/cic.mli +MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli *) @@ -226,7 +226,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|] let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] |