TODO
NUCLEO
+ - CRITICO (trovato anche da Ferruccio): typechecking di
+ cic:/Coq/ring/Ring_normalize/index_eq_prop.con
+ asserzione del nucleo (applicazione senza argomenti)
- 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
TATTICHE
+ - simplify (e altre tattiche) non debbono zeta-espandere i let-in
- tattica unfold su rel a let-in bound variables
- theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con
True.
- notazione -> Luca e Zack
- non chiudere transitivamente i moo ??
+ DEMONI E ALTRO
+ - implementare inclusione file di configurazione (perche' ora tutti
+ i demoni scopiazzano venti righe per via del getter embedded :-(
+
DONE
- library/nat/primes.ma: ex_prime ci mette un secolo il db (binding) a fare
la Mysql.exec che ritorna una lista vuota di risultati. Investigare.