Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fixpoint` with a let binder

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

1 files changed, 13 insertions, 0 deletions

diff --git a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
new file mode 100644
index 0000000000..f8298cdbdd
--- /dev/null
+++ b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
@@ -0,0 +1,13 @@
+- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments
+  in the presence of local definitions, see `#3282 <https://github.com/coq/coq/issues/3282>`_
+  (`#11132 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin).
+
+  .. example::
+
+     The following features an implicit argument after a local
+     definition. It was wrongly rejected.
+
+     .. coqtop:: in
+
+        Definition f := fix f (o := true) {n : nat} m {struct m} :=
+          match m with 0 => 0 | S m' => f (n:=n+1) m' end.