Fix for a new rapply tactic#78
Merged
spitters merged 1 commit intoOct 16, 2023
Merged
Conversation
This backwards compatible change makes math-classes work with rocq-prover/rocq#10760 by replacing all instances of `rapply` which were relying on typeclass resolution happening *before* `refine` (instead of simultaneously with it) to instead invoke `Tactics.rapply` (which is the same tactic in Coq <= 8.10, and which will be the tactic rather than the `uconstr`-taking tactic notation in Coq >= 8.11). See also rocq-prover/rocq#10760 (comment)
2 tasks
Member
|
Note that while this patch does no harm, it is not clear yet whether rocq-prover/rocq#10760 will be merged as is, and thus whether it will be necessary. |
Collaborator
|
I'm fine with the changes, but propose to wait until the discussion in rocq-prover/rocq#10760 stabilizes. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This backwards compatible change makes math-classes work with
rocq-prover/rocq#10760 by replacing all instances of
rapplywhich were relyingon typeclass resolution happening before
refine(instead ofsimultaneously with it) to instead invoke
Tactics.rapply(which is thesame tactic in Coq <= 8.10, and which will be the tactic rather than the
uconstr-taking tactic notation in Coq >= 8.11).See also rocq-prover/rocq#10760 (comment)
For reference, this changes 9 of the 34 invocations of
rapply.