Fixing rat_interlock + Add gaia in CI #798
Merged
Conversation
This file contains 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
CohenCyril
force-pushed
the
rat_interlock
branch
2 times, most recently
from
ca19e72
to
5d90cdb
Compare
|
@thery now it fails because it's too powerful https://github.com/math-comp/math-comp/pull/798/checks?check_run_id=3884025523#step:11:27 |
|
@CohenCyril that was the only problem. Commited here |
CohenCyril
force-pushed
the
rat_interlock
branch
from
5d90cdb
to
5705476
Compare
|
@CohenCyril would it be worth to add a test_rat.v in the test_suite to check everything works as planned? |
CohenCyril
force-pushed
the
rat_interlock
branch
from
5705476
to
24b8a5b
Compare
done |
|
@CohenCyril do we wait for @pi8027's review or we merge? |
pi8027
approved these changes
Oct 17, 2021
CohenCyril
added
the
kind: fix
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Motivation for this change
Fixes coq-community/gaia#4 by making sure operations on rationals produce a canonical representative of the rational (not only the ratio, but also the proof). This makes
(-1)^-1 = -1hold by reflexivity and hence fixes the breakage ingaia.CC @thery
Things done/to do
CHANGELOG_UNRELEASED.md(do not edit former entries)added corresponding documentation in the headersAutomatic note to reviewers
Read this Checklist and make sure there is a milestone.