diff options
| author | coqbot-app[bot] | 2021-04-05 12:16:42 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-05 12:16:42 +0000 |
| commit | 56c32d83cb98056492b6d1feae800bbd73d1996a (patch) | |
| tree | f9987f68d20e4d4937c0424829bc5b8f6472a9ee /doc | |
| parent | 012b8a08f142d39b2211fd52c811f830f88f2075 (diff) | |
| parent | 643c10a894c1db24dd8ab06cc4376c92ae8b7c3c (diff) | |
Merge PR #13624: Fixing #13581: missing support for let-ins in arity of inductive types for extraction
Reviewed-by: pi8027
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). |