Stream: Coq devs & plugin devs

Topic: Extraction of sort-polymorphic types in Prop


view this post on Zulip Hugo Herbelin (Feb 27 2023 at 11:29):

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