coq-0This person does not understand Coq (or does not want to program in Coq).