diff options
| author | Clément Pit-Claudel | 2019-09-12 18:27:38 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-09-12 18:27:38 -0400 |
| commit | 592f2155f97441022f6b9e238563c8d7794ce60f (patch) | |
| tree | aa2c76c9ed1ac1726f5004815ec1b3ca3a305d47 /doc/changelog/01-kernel | |
| parent | 4debcab8771f0c2f52b7697dbf2233f931f863e6 (diff) | |
| parent | 85897b6c031470d719a28754d3c02de09000c8d8 (diff) | |
Merge PR #10753: Release notes for 8.10+beta3.
Reviewed-by: cpitclaudel
Diffstat (limited to 'doc/changelog/01-kernel')
| -rw-r--r-- | doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst b/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst deleted file mode 100644 index 87e89a70f1..0000000000 --- a/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst +++ /dev/null @@ -1,30 +0,0 @@ -- Fix soundness issue with template polymorphism (`#9294 - <https://github.com/coq/coq/issues/9294>`_) - - Declarations of template-polymorphic inductive types ignored the - provenance of the universes they were abstracting on and did not - detect if they should be greater or equal to :math:`\Set` in - general. Previous universes and universes introduced by the inductive - definition could have constraints that prevented their instantiation - with e.g. :math:`\Prop`, resulting in unsound instantiations later. The - implemented fix only allows abstraction over universes introduced by - the inductive declaration, and properly records all their constraints - by making them by default only :math:`>= \Prop`. It is also checked - that a template polymorphic inductive actually is polymorphic on at - least one universe. - - This prevents inductive declarations in sections to be universe - polymorphic over section parameters. For a backward compatible fix, - simply hoist the inductive definition out of the section. - An alternative is to declare the inductive as universe-polymorphic and - cumulative in a universe-polymorphic section: all universes and - constraints will be properly gathered in this case. - See :ref:`Template-polymorphism` for a detailed exposition of the - rules governing template-polymorphic types. - - To help users incrementally fix this issue, a command line option - `-no-template-check` and a global flag :flag:`Template Check` are - available to selectively disable the new check. Use at your own risk. - - (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau - and Maxime Dénès). |