Type Classes for Mathematical Formalizations in Coq - Matthieu Sozeau Video of Type Classes for Mathematical Formalizations in Coq - Matthieu Sozeau Matthieu SozeauINRIA Paris; Member, School of MathematicsOctober 3, 2012