The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Hi, thank you, the return "trik" works with minor twiking.
However it really leave me in the total misunderstanding of why it works:

I was thinking (eq_refl optA) to produce a proof for optA=optA, not
for optA=x, moreover x looks out of
scope outside the parenthesis of the match... may be I have to study
what exactly the return does.

> Definition f (optA : option A) :=
> (match optA as x return optA = x -> nat with
>  | Some a => (fun p => O)
>  | None => (fun p => 1)
> end) (eq_refl optA).

And again,  thank you all!
Marco.