Ralf Jung (Oct 22 2020 at 11:28): Ralf Jung (Oct 22 2020 at 11:28):Is there any way at all to use (e)apply ... with (name:=val) when name mangling is enabled? It seems like that should be possible, given in particular that term (name:=val) does work with name mangling. But so far I failed to get this to work. This fails:
Set Mangle Names.
Lemma lem1 (P Q: Prop) : P -> Q -> P.
Proof. auto. Qed.
Goal True. Proof.
eapply lem1 with (Q:=True).
And speaking of with, it'd be great if someone could explain this behavior ;) (EDIT: @Pierre-Marie Pédrot already did)
Ralf Jung (Oct 22 2020 at 11:29):The inability to use with is particularly annoying since term (name:=val) unfortunately only works for implicit arguments
Ralf Jung (Oct 22 2020 at 11:33):potentially related: https://github.com/coq/coq/issues/4536
Ralf Jung (Oct 22 2020 at 11:50):for term (name:=val), a change was made to avoid refreshing names unnecessarily; I wonder if something similar could be done here?
Last updated: Oct 13 2024 at 01:02 UTC