From a81c2de033b37c22be1ca6794ab32347a9917610 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 17 Nov 2019 09:39:50 +0100 Subject: Fixing bugs in the computation of implicit arguments for fix with a let binder. --- .../11132-master+fix-implicit-let-fixpoint-bug3282.rst | 1 + 1 file changed, 1 insertion(+) create mode 100644 doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst (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 new file mode 100644 index 0000000000..3ee3444c60 --- /dev/null +++ b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst @@ -0,0 +1 @@ +- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments in the presence of local definitions, see #3282 (`#11132 `_, by Hugo Herbelin). -- cgit v1.2.3 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