+- controllo per script modificato o meno prima di uscire -> Gares
+- LApply deve prendere in input gli identificatori che va a generare;
+ lascio a Ferruccio la scelta della sintassi concreta -> Ferruccio
+- fare tornare a matitac -1 quando lo stato finale e'
+ diverso da No_proof, non eseguire comandi quando lo
+ stato e' diverso da No_proof -> CSC
+- uri_of_term and term_of_uri: cambiare il tipo per far
+ tornare delle uri!!! -> CSC