"git-rts@gitlab.mpi-sws.org:proux/iris.git" did not exist on "c568ece0b549f26d48fc961cd80e2f0e0af46969"
notypeclasses apply: fix comment
The implementation actually uses eval hnf
, so it is not purely syntactic.
I don't know what behavior we want, but clearly docs and implementation should match... and for the o*
tactics, unfolding seems to work better; e.g. we have existing uses of oinversion
on statements of the form ... → not _
that would otherwise break.
Edited by Ralf Jung
Merge request reports
Activity
Please register or sign in to reply