The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/23/2012 10:35 AM, Adam Chlipala wrote:
> It's a good thing that Coq rejects this definition, since _any_ 
> definition of [IsSome_extract] would be breaking basic rules about 
> what [Prop] means, and could even lead to logical inconsistency! ;)
>
> A type in [Prop] is meant to have no computational content, and yet 
> here you are trying to extract a potentially computational value out 
> of one of these.

Thinking about this more, I see that you were _trying_ to write the 
definition differently, to avoid this problem.  Sorry for the confusion.