program_logic/iris.v · be24297e3f28d057c39ceff6c1ec4a9942c08054 · Simcha van Collem / Iris

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago

Do not use [ucmraT]s as argument of inG. · be24297e

Since [inG] ranges over [cmraT]s, using an [ucmraT]s results in
[ucmra_cmraR] coercions that slow down type checking.

This commit improves the compilation time of thread_local.v by 40%.

be24297e

History

Do not use [ucmraT]s as argument of inG.

Robbert Krebbers authored 8 years ago

Since [inG] ranges over [cmraT]s, using an [ucmraT]s results in
[ucmra_cmraR] coercions that slow down type checking.

This commit improves the compilation time of thread_local.v by 40%.