The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Edsko de Vries wrote:
> That was great! Thanks a million. Using chapter 9 from your book I 
> could now finish the proof. For posteriority's sake, the completed 
> script is below. By the way, are these axioms about equality 
> implementable? Or does extraction become impossible when one of these 
> axioms is used?

I'm guessing you mean the [Eqdep] and [JMeq] axioms.  These are in 
[Prop], so it doesn't make sense to talk about "implementing them for 
extraction," since any Coq realization would be erased, anyway.  
Programs that use them extract to working OCaml code.