Critical bug fixed: the get_cooked_obj was called on an object that was not

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

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 0d3fa1aec319fe77d0a7dc36d8853606719a2c3d..a3d87835ad04ef286b35a13233a8fb0ede2d3fca 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -1,7 +1,5 @@
 TODO
   NUCLEO
-  - CRITICO: quando l'environment non e' trusted non compila la library di
-    matita!!!
   - PREOCCUPANTE: per 
     inductive i : Prop := K : True (*-> i*) -> i.
     noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON
@@ -112,6 +110,8 @@ TODO
     i demoni scopiazzano venti righe per via del getter embedded :-(
 
 DONE
+- CRITICO: quando l'environment non e' trusted non compila la library di
+  matita!!! -> Gares, CSC
 - bug di unsharing -> CSC
 - CRITICO (trovato anche da Ferruccio): typechecking di
   cic:/Coq/ring/Quote/index_eq_prop.con