[xvilka]

It's notable, that Coq has more libraries and useful extensions. And they merged Ltac2 into the master, so tactics writing should be better soon.