apply foo
leaves typeclass goals solved by apply (foo _)
#12617
Labels
kind: bug
An error, flaw, fault or unintended behaviour.
part: apply
The tactics apply, eapply, etc.
part: typeclasses
The typeclass mechanism.
Description of the problem
It seems enough that
foo
isLemma foo P {!SomeTypeClass P} : ...
.An example is
big_sepL2_nil'
in Iris which isdiscussed in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/468#note_53032.
Fixing this would probably break compatibility, especially with code like
apply foo. apply _.
The text was updated successfully, but these errors were encountered: