Adding changelog for #15498

coq · Jan 17, 2022 · 0a42adf · 0a42adf
1 parent f4bea91
commit 0a42adf
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/doc/changelog/01-kernel/15498-master+fix15451-incompleteness-guard-condition.rst b/doc/changelog/01-kernel/15498-master+fix15451-incompleteness-guard-condition.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  cases of incompletenesses in the guard condition for fixpoints in
+  the presence of cofixpoints or primitive projections
+  (`#15498 <https://github.com/coq/coq/pull/15498>`_,
+  fixes `#15451 <https://github.com/coq/coq/issues/15451>`_,
+  by Hugo Herbelin).