-
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.
e3cb5b14
This way we avoid the env_cbv tactic unfolding string related stuff that appears in the goal and hypotheses of the proof mode.