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: Nov 29 2023 at 18:01 UTC