From 3a651d1c69ca0c69bc07263f507c768f59ea6d0f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 13:02:44 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -- 2.39.2