From 570ffaf1ee3c7ca4a58051c87b61f1058eb9f1f3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 16 Sep 2019 20:46:29 +0200 Subject: 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. --- doc/changelog/02-specification-language/10758-fix-10757.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/02-specification-language/10758-fix-10757.rst (limited to 'doc') 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 + `_, by Gaëtan Gilbert, fixing + `#10757 `_ reported by + Xavier Leroy). -- cgit v1.2.3