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 /engine | |
| parent | 988e195c2cd0d97b664193bf1c83c3da2b380f7c (diff) | |
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/uState.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index ff85f09efa..abd5f2828f 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -39,7 +39,7 @@ type t = uctx_weak_constraints : UPairSet.t } -let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes +let initial_sprop_cumulative = UGraph.set_cumulative_sprop true UGraph.initial_universes let empty = { uctx_names = UNameMap.empty, LMap.empty; @@ -57,11 +57,11 @@ let elaboration_sprop_cumul = ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true let make ~lbound u = - let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in - { empty with - uctx_universes = u; - uctx_universes_lbound = lbound; - uctx_initial_universes = u} + let u = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) u in + { empty with + uctx_universes = u; + uctx_universes_lbound = lbound; + uctx_initial_universes = u} let is_empty ctx = ContextSet.is_empty ctx.uctx_local && @@ -547,10 +547,11 @@ let emit_side_effects eff u = merge_seff u uctx let update_sigma_env uctx env = - let univs = UGraph.make_sprop_cumulative (Environ.universes env) in + let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in let eunivs = - { uctx with uctx_initial_universes = univs; - uctx_universes = univs } + { uctx with + uctx_initial_universes = univs; + uctx_universes = univs } in merge_seff eunivs eunivs.uctx_local |