diff options
| author | Gaëtan Gilbert | 2019-09-16 20:46:29 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-09-16 20:59:35 +0200 |
| commit | 570ffaf1ee3c7ca4a58051c87b61f1058eb9f1f3 (patch) | |
| tree | 4a3b4845b69c8f452706b38a2e933106c3778b21 /doc | |
| parent | 3d7de72f45ae2f8bcedbe1db0eb8870e58757b45 (diff) | |
Fix #10757: Program Fixpoint uses "exists" for telescopes
This helps extraction by not building sigT which can lower to Prop by
template polymorphism.
Bug #10757 can probably still be triggered by using module functors to
hide that we're using Prop from Program Fixpoint but that's probably
unfixable without fixing extraction vs template polymorphism in
general.
In passing we notice that Program doesn't know how to telescope SProp
arguments, we would need a bunch of variants of sigma types to deal
with it (or use Box?) so let's figure it out some other time.
We also reuse the universe instance to avoid generating a bunch of
short-lived universes in the universe polymorphic case.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/10758-fix-10757.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/10758-fix-10757.rst b/doc/changelog/02-specification-language/10758-fix-10757.rst new file mode 100644 index 0000000000..4cce26aedc --- /dev/null +++ b/doc/changelog/02-specification-language/10758-fix-10757.rst @@ -0,0 +1,5 @@ +- ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes + involving ``Prop`` types (`#10758 + <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing + `#10757 <https://github.com/coq/coq/issues/10757>`_ reported by + Xavier Leroy). |