From 17532fac9ddba4c59f8afcdd7f69556b35909a9d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 10:08:37 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 76d0f873a..56b1ef4ca 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -1,5 +1,7 @@ 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 -- 2.39.2