Interestingly, the author did a dissertation using Coq, so I wonder if he thinks that it's not really suitable.
There has been a lot of development on the Coq proof assistant since then. I don't imagine that working with Coq in 2008 was particularly pleasant. :)
O'Connor gave a nice talk at TPHol's which I attended: https://arxiv.org/abs/cs/0505034
Keeping up with Coq shouldn't have been too difficult for him.