The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi all,
When we have some coercions between types, the command "Print Coercion 
Paths A B" checks if there exists a coercion path between types A and B. 
I wonder if there is a mean to get back the result of this command 
inside the Coq code (e.g., in a function) to further achieve some 
pattern matching. If anyone has an idea?
Thanks a lot,
Richard

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard