From 7df37822980666c51109205dca8df99f3b81c4fb Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Mon, 18 Jan 2021 12:15:40 +0100
Subject: Add changelog

---
 doc/changelog/04-tactics/13699-fix13579.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/04-tactics/13699-fix13579.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/13699-fix13579.rst b/doc/changelog/04-tactics/13699-fix13579.rst
new file mode 100644
index 0000000000..9cf62fb595
--- /dev/null
+++ b/doc/changelog/04-tactics/13699-fix13579.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  :tacn:`simpl` and :tacn:`hnf` now reduce primitive functions
+  on primitive integers, floats and arrays
+  (`#13699 <https://github.com/coq/coq/pull/13699>`_,
+  fixes `#13579 <https://github.com/coq/coq/issues/13579>`_,
+  by Pierre Roux).
-- 
cgit v1.2.3