(**********************************************************************)
TODO
+- Guardare il commento
+ (*CSC: this code is suspect and/or bugged: we try first without reduction
+ and then using whd. However, the saturate_term always tries with full
+ reduction without delta. *)
+ in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply
+ oltre che di bug!
+- Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo
+ lockato!
- Dare errore significativo al posto di NotWellTypedInterpreation
- Implementare menu edit: find/replace/cut/copy/undo/etc.
- Bug vari nella generazione dei principi di eliminazione: