The Coq mailing list

[quanta AT sdf.lonestar.org]

I would like to add the axioms from Martin Hofmann, A Simple Model for 
Quotient
Types to Coq. The Axiom command does not seem to be enough to do this, because
it only lets me defined now type judgements, I must also add new reductions to
the equational theory of Coq. Sadly I am not skilled enough at Ocaml to add
this directly to the ocaml files but maybe someone here can suggest an easier
route. Thank you all for your responses.