From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 13:02:44 +0000 (+0000) Subject: ... X-Git-Tag: V_0_1_2_1~115 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a651d1c69ca0c69bc07263f507c768f59ea6d0f;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 3d3fb2702..0d3fa1aec 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -79,8 +79,8 @@ TODO in sync - fattorizzare codice fra MatitaEngine e DisambiguatePp (dove, fra l'altro, ora io (=CSC) ho messo anche un parser!!!) - - integrare nuova contrib ferruccio nel bench notturno; guardare bug - generazione principi di eliminazione + - integrare nuova contrib ferruccio nel bench notturno e rilocarla in + contribs o qualcosa del genere - bug "Warn: baseuri cic:/matita/higher_order_defs/ordering is not empty" mentre si compila Z/times.ma. Il bug sembra essere transiente. - in MatitaEngine unificare/rimuovere eval_string, eval_from_stream e @@ -112,6 +112,7 @@ TODO i demoni scopiazzano venti righe per via del getter embedded :-( DONE +- bug di unsharing -> CSC - CRITICO (trovato anche da Ferruccio): typechecking di cic:/Coq/ring/Quote/index_eq_prop.con asserzione del nucleo (applicazione senza argomenti). -> CSC