]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matita.txt
* Part of matita that used to deal with the library moved into ocaml/library
[helm.git] / helm / matita / matita.txt
index cac073c2940fe7c20c7506e4a606315d0b42e4e7..f26f95c3c8fe5049048bf8a44487234866727aa1 100644 (file)
@@ -1,3 +1,10 @@
+Ferruccio ha cambiato matita.lang:
+>      <keyword>iforall</keyword>
+>      <keyword>iexists</keyword>
+
+- possibile bug cut&paste di pattern profondi nelle ipotesi: secondo
+  me sbaglia il nome dell'ipotesi!
+
 TODO
   NUCLEO
    - http://mowgli.cs.unibo.it:58084/proofCheck?uri=cic:/Coq/Reals/Rtopology/interior_P3.con