(**********************************************************************)
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