Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[micromega] Add missing support for implb #13715

Merged
merged 1 commit into from Jan 7, 2021
Merged

[micromega] Add missing support for implb #13715

merged 1 commit into from Jan 7, 2021

Conversation

fajb
Copy link
Contributor

@fajb fajb commented Jan 5, 2021

This PR adds implb to the boolean operators recognised by lia.

Kind: bugfix

  • updated test-suite

@fajb fajb requested a review from a team as a code owner January 5, 2021 10:11
@gares gares added this to the 8.14+beta1 milestone Jan 5, 2021
@vbgl vbgl self-assigned this Jan 6, 2021
Copy link
Contributor

@vbgl vbgl left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this change be documented (changelog or user’s manual)?

@vbgl vbgl added the part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic. label Jan 6, 2021
@fajb
Copy link
Contributor Author

fajb commented Jan 6, 2021

@vbgl I added a changelog entry. The code is now in sync with the documentation...

@gares gares added the kind: fix This fixes a bug or incorrect documentation. label Jan 6, 2021
@vbgl vbgl merged commit ad9fdf7 into coq:master Jan 7, 2021
@fajb
Copy link
Contributor Author

fajb commented Jan 7, 2021

Thanks @vbgl

@fajb fajb deleted the lia_implb branch January 12, 2021 13:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: fix This fixes a bug or incorrect documentation. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants