aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/04-tactics
diff options
context:
space:
mode:
authorBESSON Frederic2021-01-05 10:05:47 +0100
committerBESSON Frederic2021-01-06 10:39:07 +0100
commitac64cad9e6c0496afc600380d5c21fd1129db400 (patch)
tree0e69ed3a9444572a8eed170e331497bcfa3f1cca /doc/changelog/04-tactics
parent8c7457e18de2fb5be89f22c76ac59541345d1d5c (diff)
[micromega] Add missing support for `implb`
Diffstat (limited to 'doc/changelog/04-tactics')
-rw-r--r--doc/changelog/04-tactics/13715-lia_implb.rst2
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).