diff options
| author | Hugo Herbelin | 2020-12-12 12:22:18 +0100 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2021-04-04 18:01:25 +0900 |
| commit | 950015d13ceb0c65c2eda42578788c8fe7ea31f1 (patch) | |
| tree | f2df861ebffcdb413116dfb05d067dc9ab2147f0 /doc | |
| parent | a265c1ad912b4940861ec27efd09e5b20d33233c (diff) | |
Adding change log for #13624.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst new file mode 100644 index 0000000000..6a34f5a70e --- /dev/null +++ b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Failure of extraction in the presence of inductive types with local + definitions in parameters + (`#13624 <https://github.com/coq/coq/pull/13624>`_, + fixes `#13581 <https://github.com/coq/coq/issues/13581>`_, + by Hugo Herbelin). |