diff options
| author | Vincent Laporte | 2021-01-07 09:58:51 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2021-01-07 09:58:51 +0100 |
| commit | ad9fdf76897ada659dc1ca6d2d931452f6361f93 (patch) | |
| tree | 2fa1044833d278136f6c706b9453ef7be41bc3a6 /doc | |
| parent | 30f497eaf34f2cf641c3fe854fc9066ae19eea67 (diff) | |
| parent | ac64cad9e6c0496afc600380d5c21fd1129db400 (diff) | |
Merge PR #13715: [micromega] Add missing support for `implb`
Reviewed-by: vbgl
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/13715-lia_implb.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/13715-lia_implb.rst b/doc/changelog/04-tactics/13715-lia_implb.rst new file mode 100644 index 0000000000..dd61872342 --- /dev/null +++ b/doc/changelog/04-tactics/13715-lia_implb.rst @@ -0,0 +1,2 @@ +- **Added:** + :tacn:`lia` supports the boolean operator `Bool.implb` (`#13715 <https://github.com/coq/coq/pull/13715>`_, by Frédéric Besson). |