This MR is a potential solution for https://github.com/coq/coq/issues/5698
We currently declare primitive projections, e.g., those of the BI class, as simpl never. Our unseal tactics unfold these using unfold primproj; simpl which used to work prior to Coq 5698, but relied on unexpected behavior of simpl.
Looking at the discussion in Coq 5698, it seems the Coq developers are working on bigger changes to primitive projections and it will be hard to support unfolding simpl never primitive projections in a backwards compatible way. This MR therefore gets rid of using unfold, but states explicit unfolding lemmas and rewrites using those.
TODO:
-
Adapt siProp -
Adapt monPred -
Figure out if there's a good way to make sure that users don't accidentally use these lemmas, and preferably don't find them using Search.