Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Set Primitive Projections.
Set Implicit Arguments.
Set Universe Polymorphism.
Record category :=
{ ob :> Type;
hom : ob -> ob -> Type
}.
Record foo := { C : category; x : ob C; y :> hom x x }.
(* Toplevel input, characters 20-75:
Error: Cannot find the target class. *)