From ac64cad9e6c0496afc600380d5c21fd1129db400 Mon Sep 17 00:00:00 2001
From: BESSON Frederic
Date: Tue, 5 Jan 2021 10:05:47 +0100
Subject: [micromega] Add missing support for `implb`

---
 doc/changelog/04-tactics/13715-lia_implb.rst | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 doc/changelog/04-tactics/13715-lia_implb.rst

(limited to 'doc')

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).
-- 
cgit v1.2.3