I don't think working with Coq has ever or will ever be particularly pleasant :-) O'Connor gave a nice talk at TPHol's which I attended: https://arxiv.org/abs/

I don't think working with Coq has ever or will ever be particularly pleasant :-) O'Connor gave a nice talk at TPHol's which I attended: https://arxiv.org/abs/cs/0505034 https://arxiv.org/abs/cs/0505034 Keeping up with Coq shouldn't have been too difficult for him.