coq
Add SSReflect contextual pattern `UNDER`
Close #11118
This PR proposes a simpler workaround than PR https://github.com/coq/coq/pull/11200.
Cc @gares @CohenCyril @proux01 @mrhaandi FYI
- [x] Added / updated test-suite.
- [x] Added changelog.
- [x] Added / updated documentation.
Thanks for reviving this, Erik. I like the fact that this approach is simpler, but it requires the user to understand what goes wrong and it is not easy to explain. For example the changelog entry is unclear to me (if one does not know the implementation of under).
I'm wondering if we could instead hide the evar as in:
a : T
_rhs_ : S := ?123
=============
@Under_rel S (expression) _rhs_
In this way the evar and its local context are hidden. Would this work? If not I'll just click merge ;-)
@gares thanks for your comment!
I'm wondering if we could instead hide the evar as in: (...)
Yes I was also thinking about this idea, but I didn't try it... (and AFAIAC, I won'd be able to experiment this before the end of the month).
Would this work? If not I'll just click merge ;-)
Thanks. I don't know yet, but I agree this would be worth it to try. So let's postpone merging this PR for the moment...
What was the issue with the nomatch idea discussed in https://github.com/coq/coq/issues/11118#issuecomment-559148731 it sounds like a much better solution?
That would also work but needs to be implemented, and can be used outside of the under tactic. What I propose here is way more limited, but seems trivial to implement. What Erik proposes is implemented, but requires the user to do something in some situations that are not so easy to explain.
That would also work but needs to be implemented, and can be used outside of the under tactic.
Just to correct: a prototype has already been implemented:
https://github.com/coq/coq/pull/11200
but the implementation looked nontrivial and it still needs to be refined (read: fixed) to fully work... but if it looks nicer to you, maybe it would be worth it to put forth #11200 anew...