Stream: Coq devs & plugin devs

Topic: SProp breaks subject reduction?

Jason Gross (Mar 26 2021 at 20:43):

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

Enrico Tassi (Mar 26 2021 at 20:44):

This one is for @Gaëtan Gilbert

Jason Gross (Mar 26 2021 at 20:46):

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

Last updated: Apr 16 2024 at 17:01 UTC