Allow open terms in "apply ->" and "apply <-" (fix #18177). #18946
Conversation
In particular, these tactics can now be used with a symbol that has some implicit arguments.
silene
added
part: ltac
coqbot-app
bot
removed
the
request: full CI
| @@ -0,0 +1,7 @@ | |||
| - **Changed:** | |||
| When used with a direction :n:`->` or :n:`<-`, :tacn:`apply` now accepts an open term, | |||
| assuming its holes can be inferred during application, as was already the case for plain | |||
There was a problem hiding this comment.
I'm not sure what the precise meaning of "assuming" is supposed to be here.
For instance if we do
Axiom foo : unit -> True <-> True.
Goal True.
apply <- (foo _).in master it fails and with this PR it succeeds leaving a shelved unit goal.
There was a problem hiding this comment.
Good catch. I should trust my Ltac reading skills less.
There was a problem hiding this comment.
Sure, but note that the following one succeeds on master too.
Axiom foo : unit -> True <-> True.
Goal True.
let v := open_constr:(foo _) in apply <- v.So, this pull request is not adding some new semantic behaviors, it is just removing a syntactic limitation.
If you think this will make the changelog clearer, I can stop the entry just after "open term".
There was a problem hiding this comment.
Not sure how that matters, you can do regular apply with a ltac-bound open_constr too.
There was a problem hiding this comment.
@silene, IMO the least surprising behavior would be for apply -> and apply <- to match that of apply:
Axiom foo : unit -> True <-> True.
Goal True.
apply (foo _). (* Error: Cannot infer this placeholder of type "unit". *)
There was a problem hiding this comment.
Everybody agrees, and if you know how to do that, feel free to implement it.
There was a problem hiding this comment.
I made another attempt at https://github.com/andres-erbsen/coq/tree/fix-18177; it passes both tests so far
In particular, these tactics can now be used with a symbol that has some implicit arguments.
Fixes / closes #18177