diff options
| author | Hugo Herbelin | 2019-11-21 12:21:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-21 12:26:13 +0100 |
| commit | 7255c262c6cc9b3153acf9d2f694196f4e9c10e6 (patch) | |
| tree | 76205f3c0c353cfd3b6baefac882c4d9c9cd9831 | |
| parent | a81c2de033b37c22be1ca6794ab32347a9917610 (diff) | |
Update doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
| -rw-r--r-- | doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst | 14 |
1 files changed, 13 insertions, 1 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 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 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin). +- 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. |