From 7255c262c6cc9b3153acf9d2f694196f4e9c10e6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 21 Nov 2019 12:21:34 +0100 Subject: Update doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst Co-Authored-By: Théo Zimmermann --- .../11132-master+fix-implicit-let-fixpoint-bug3282.rst | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'doc') 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 index 3ee3444c60..f8298cdbdd 100644 --- 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 @@ -1 +1,13 @@ -- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments in the presence of local definitions, see #3282 (`#11132 `_, by Hugo Herbelin). +- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments + in the presence of local definitions, see `#3282 `_ + (`#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. -- cgit v1.2.3