theories/bi/lib/atomic.v · 3bd431139ac94a87fa8ac2d814a9d4d60a5a91af · Abhishek Anand / Iris

Forked from Iris / Iris

Source project has a limited visibility.

6 years ago

move the reduction control of the proofmode to its own file and tweak it · 3bd43113

Ralf Jung authored 6 years ago

* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics
* use reduction-controlled `pm_default` for proofmode accessors

3bd43113

History

move the reduction control of the proofmode to its own file and tweak it

Ralf Jung authored 6 years ago

* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics
* use reduction-controlled `pm_default` for proofmode accessors