Skip to content

notypeclasses apply: fix comment

Ralf Jung requested to merge ralf/notypeclasses-apply-docs into master

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

Loading