From: Claudio Sacerdoti Coen Date: Fri, 8 Jul 2005 09:20:20 +0000 (+0000) Subject: ... X-Git-Tag: pre_notation~81 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44ac461fc8dcaffd51476e53952551783df32fbe;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 6310a8f71..94e17c62d 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,6 +2,7 @@ (**********************************************************************) TODO +- assiomi - Guardare il commento (*CSC: this code is suspect and/or bugged: we try first without reduction and then using whd. However, the saturate_term always tries with full