Stream: Coq devs & plugin devs

Topic: SProp breaks subject reduction?


view this post on Zulip Jason Gross (Mar 26 2021 at 20:43):

Is it known that subject reduction in Coq is broken in the presence of SProp?

view this post on Zulip Enrico Tassi (Mar 26 2021 at 20:44):

This one is for @Gaƫtan Gilbert

view this post on Zulip Jason Gross (Mar 26 2021 at 20:46):

Reported as https://github.com/coq/coq/issues/14015


Last updated: Oct 16 2021 at 02:03 UTC