From 3687c3fdcf2edd7b8e7f7408d9a8ee8706fd16a9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2020 14:32:59 +0100
Subject: Add changelog for #13383.

---
 .../13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst       | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst

diff --git a/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst b/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst
new file mode 100644
index 0000000000..c0e5a81641
--- /dev/null
+++ b/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Using :n:`{wf ...}` in local fixpoints is an error, not an anomaly
+  (`#13383 <https://github.com/coq/coq/pull/13383>`_,
+  fixes `#11816 <https://github.com/coq/coq/issues/11816>`_,
+  by Hugo Herbelin).
-- 
cgit v1.2.3