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.
The main thing with supporting std++ 1.7 and Coq 8.15.0 was another typeclass resolution problem. In the 4 refinement goals, it resolves to
(@ptr_type_check K (@rank_eq_dec K (@int_coding K (@env_type_env K H))) H)
instead of(@ptr_type_check K EqDecision0 H)
. I think this change is caused by Coq 8.15, but I have trouble figuring out why.The other two are small renames. These do prevent backwards compatibility.