From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 20 Sep 2005 16:51:43 +0000 (+0000)
Subject: ...
X-Git-Tag: LAST_BEFORE_NEW~74
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b3cd0302d013a8590f20b2c51f16e5167dcc210f;p=helm.git

...
---

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