+ (* TODO Zack FINQUI
+ * bisogna rivedere la grammatica di tatticali/comandi
+ * molti comandi (o addirittura tutti tranne Theorem) hanno senso anche nello
+ * stato proof, e' quindi un casino parsare la phrase. Un'idea potrebbe essere
+ * quella di tentare di parsare una tattica e se il parsing fallisce provare a
+ * parsare un comando (BLEAARGH). Oppure si puo' aggiungere una possibile entry
+ * nella grammatica delle tattiche che punti ad un comando (RI-BLEAARGH).
+ * Oppure boh ...
+ *)