From b3cd0302d013a8590f20b2c51f16e5167dcc210f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 20 Sep 2005 16:51:43 +0000
Subject: [PATCH] ...

---
 helm/matita/matita.txt | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 3947bbbad..060431d89 100644
--- 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
-- 
2.39.2