Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
This way we avoid the env_cbv tactic unfolding string related stuff that appears in the goal and hypotheses of the proof mode.
Robbert Krebbers authoredThis way we avoid the env_cbv tactic unfolding string related stuff that appears in the goal and hypotheses of the proof mode.
