diff options
| author | Frédéric Besson | 2020-05-11 11:59:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-14 11:26:41 +0200 |
| commit | f8e91cb0a227a2d0423412e7533163568e1e9fdf (patch) | |
| tree | 3a16a91e7167cb942686ab6657b76e3b86c151df /doc/changelog | |
| parent | 13e8d04b2f080fbc7ca169bc39e53c8dd091d279 (diff) | |
[micromega] native support for boolean operators
The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/04-tactics/11906-micromega-booleans.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/11906-micromega-booleans.rst b/doc/changelog/04-tactics/11906-micromega-booleans.rst new file mode 100644 index 0000000000..39d1525ac3 --- /dev/null +++ b/doc/changelog/04-tactics/11906-micromega-booleans.rst @@ -0,0 +1,4 @@ +- **Added:** + :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`. + (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) + (`#11906 <https://github.com/coq/coq/pull/11906>`_, by Frédéric Besson). |