...

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 3947bbbadedd8d2c79f1d6bdfd47cc200b88c020..060431d8900ab32d97e3c53b4bc72e7236f6e5c3 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -77,6 +77,9 @@ TODO
   - riattaccare hbugs (brrr...) -> Zack
 
   GUI LOGICA
+  - proposta di Zack: NON calcolare (ed esportare) per default gli inner-types;
+    aggiungere un'opzione per questo a matitac (riduce drasticamente il tempo
+    di qed)
   - la funzione alias_diff e' lentissima (anche se CSC l'ha accellerata di
     un fattore 3x) e puo' essere evitata: chi vuole aggiungere alias (la
     disambiguazione, il comando "alias" e l'add_obj) deve indicare