With a colleague, we are facing again the issue of extraction forbidding to use sort-polymorphic singleton inductive types landing in Prop. This decided me to start experimenting the automatic insertion of coercions discussed in #13486. This seems to work well so far, fixing also the bug reported in #13486.
Last updated: Oct 13 2024 at 01:02 UTC