<br><div class="gmail_quote">On Thu, Aug 25, 2011 at 3:33 PM, Pavel Perikov <span dir="ltr"><<a href="mailto:perikov@gmail.com">perikov@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi, list!<br>
<br>
What was the semantics of Prop in versions prior to 2.2.8? (release note states it was removed). Was it impredicative as in Coq? What was the reason for it to be removed?<br></blockquote><div><br></div><div>It was an experimental universe whose inhabitants (if you enabled the flag --proof-irrelevance) were syntactically restricted to have at most one element. The idea was that you could get proof irrelevance for Prop cheaply. It didn't quite work out, so we removed it.</div>
<div><br></div><div>/ Ulf</div></div>