search

mit-plv / bbv

Bedrock Bit Vector Library
MIT License
27 stars 23 forks source link

compatibility with Coq PR #11906 #31

Closed fajb closed 4 years ago

fajb commented 4 years ago

Coq PR https://github.com/coq/coq/pull/11906 extends lia with support for boolean operators. This has the consequence that intuition is able to perform some boolean reasoning e.g. true = false -> 0 = 1. The PR removes (redundant) calls to intuition.

samuelgruetter commented 4 years ago

This is yet another instance of getting bitten by the default auto with * in intuition and firstorder. We should really stop using them without an explicit leaf tactic.

On the other hand, removing redundant invocations of intuition is an improvement too, so I'm merging this, thanks @fajb!