The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> This tells that [cond] is a function which receives an argument of type C.
> But what is it meanings?

It means that it returns the proof object stored under the `cond' field.

> If the argument x is of type C, it is already
> verified that [cond x] is true!

Are you confusing booleans with objects of type Set, maybe?


        Stefan