Matita vs Coq

The system shares a common look&feel with the Coq proof assistant and its graphical user interface. The two systems have the same logic, very close proof languages and similar sets of tactics. Moreover, Matita is compatible with the library of Coq. From the user point of view the main lacking features with respect to Coq are:

Still from the user point of view, the main differences with respect to Coq are: