...

[helm.git] / helm / matita / matita.txt

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 9a53f4cc6bff079d0cf76ba5176eb4bbbab0ff95..d1f44f3e651103c14bf7ecd9a3efb9d431679602 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -2,6 +2,10 @@
 (**********************************************************************)
 
 TODO
+- Bug: non disambigua
+  inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
+  perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug
+  stupido da qualche parte
 - preoccupante: per 
   inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
   noi generiamo anche i_rec e i_rect che Coq non genera (e che NON dovrebbero