theories/base_logic/upred.v · a5063f60b461e099a5b029dd0c2ae43e8e45e43e · Paolo G. Giarrusso / iris

Forked from Iris / Iris

Source project has a limited visibility.

7 years ago

Enable primitive projections for bi.interface. · a5063f60

This gives a 25% speedup on some files (e.g. boxes).

This commit contains some hacks to work arround Coq issue #5699.

This commit requires Coq v8.7 together with

  https://github.com/coq/coq/pull/1006

a5063f60

History

Enable primitive projections for bi.interface.

Robbert Krebbers authored 7 years ago

This gives a 25% speedup on some files (e.g. boxes).

This commit contains some hacks to work arround Coq issue #5699.

This commit requires Coq v8.7 together with

  https://github.com/coq/coq/pull/1006