Matita vs Coq

The system shares a common look&feel with the Coq proof assistant and its graphical user interface. The two systems have variants of the same logic, close proof languages and similar sets of tactics. 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: