Barras, B. Sets in Coq, Coq in Sets. JFR 2010, 3, 29-48.