]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2013-04-17 Wilmer RicciottiFixes a bug which caused Meta_not_found exceptions...
2013-04-16 Ferruccio Guidimilestone update in basic_2!
2013-04-16 Ferruccio Guidi- we commit just the components before "reducibility"
2013-04-15 Ferruccio Guidiuncommited file found :)
2013-04-10 matitawebcommit by user andrea
2013-04-10 matitawebcommit by user andrea
2013-04-10 matitawebcommit by user andrea
2013-04-10 matitawebcommit by user andrea
2013-04-09 Wilmer RicciottiFixes a bug that caused an assertion failure when no...
2013-04-08 Claudio Sacerdoti... Patch by Paolo Tranquilli. It fixes the following probl...
2013-04-08 matitawebcommit by user andrea
2013-04-07 Ferruccio Guidiupdate in basic_2 and apps_2
2013-04-07 Ferruccio Guidi- new component for restricted computation (delta,...
2013-04-05 Ferruccio Guidiupdate in basic_2
2013-04-05 Ferruccio Guidi- parallel substitution reaxiomatized
2013-03-20 Ferruccio Guidi- probe: recursive removal of empty directories
2013-03-18 Ferruccio Guidimissing or rootless dependences now don't break the...
2013-03-18 Ferruccio Guidisome additions
2013-03-18 Ferruccio Guidiupdate in basic_2
2013-03-18 Ferruccio Guidia file was added by mistake
2013-03-18 Ferruccio Guidi- more understanding of the "big tree" reduction step
2013-03-17 Ferruccio Guidisfr renamed as lbotr and its symbol changed according...
2013-03-17 Ferruccio Guidinotational change for lsubr:
2013-03-17 Ferruccio Guidilsubs renamed as lsubr
2013-03-17 Ferruccio Guidinotational change for snv and lsubsv: inverted "!"...
2013-03-16 Ferruccio Guidimilestone in basic_2!
2013-03-16 Ferruccio Guidi- lambdadelta: last recursive part of preservation...
2013-03-14 Ferruccio Guidithis is the real update :)
2013-03-14 Ferruccio Guidiupdate in basic_2
2013-03-14 Ferruccio Guidi- main proof case closed in the 4th component of preser...
2013-03-13 Ferruccio Guidi- lambdadelta: third recursive part of preservation...
2013-03-11 Ferruccio Guidimore results on lenv refinement for stratified native...
2013-03-11 Ferruccio Guidibugfix in web tables
2013-03-11 Ferruccio Guidisome bugs fixed
2013-03-11 Ferruccio Guidi- xslt and Makefile improved, web pages regenerated
2013-03-11 Andrea AspertiChpater 4 and 5
2013-03-10 Ferruccio Guidi- improved Makefile esp. with the "trim" function
2013-03-10 Andrea Aspertichapters 2 e 3
2013-03-10 Ferruccio Guidiwe removed a useless assertion that was forcing matita...
2013-03-09 Ferruccio Guidi- update in basic_2
2013-03-09 Ferruccio Guidibasic_2_src.tbl was not updated :(
2013-03-09 Ferruccio Guidi- lenv refinement for stratified native validity redefined
2013-03-08 Ferruccio Guidisecond recursive part of preservation finally proved!
2013-03-08 Ferruccio Guidiupdate in basic_2
2013-03-08 Ferruccio Guidiimproved "big treee" computation allows to close a...
2013-03-04 Claudio Sacerdoti... Bug fixed: let-rec defined propositions are no longer...
2013-03-03 Ferruccio Guidiupdate in basic_2
2013-03-03 Ferruccio Guidi- lambdadelta: we removed focalized reduction from...
2013-02-28 Ferruccio Guidiupdate in basic_2
2013-02-28 Ferruccio Guidi- lambdadelta: first recursive part of preservation...
2013-02-28 Andrea Aspertichapter2 revisited
2013-02-27 Claudio Sacerdoti... Quick patch: the maxmeta is now pushed/popped when...
2013-02-27 Claudio Sacerdoti... Quick patch: the maxmeta is now pushed/popped when...
2013-02-27 Claudio Sacerdoti... Bug fixed: composite coercions were not extracted.
2013-02-27 Claudio Sacerdoti... Bug fixed that reveals a new one: in case of inductive...
2013-02-27 Claudio Sacerdoti... Ferruccio's removal of objects commented out because...
2013-02-27 Andrea AspertiChapter 1 revisited
2013-02-25 Ferruccio Guidiwhen we serialize the contents of a .ma, we remove...
2013-02-24 Ferruccio Guidi- xhtbl: now double quotes can appear in string literals
2013-02-24 Ferruccio Guidi- nUri : added Sets of uris for use in "probe"
2013-02-22 Ferruccio Guidiupdate in basic_2
2013-02-22 Ferruccio Guidi- "big tree" order implemented
2013-02-18 Ferruccio Guiditrace added in a failing invocation of auto :-(
2013-02-18 Ferruccio Guidiupdate in basic_2
2013-02-18 Ferruccio Guidisubstitution lemma for stratified native validity!
2013-02-15 Ferruccio Guidiupdate in basic_2 summary
2013-02-15 Ferruccio Guidiwe rephrased sstas in terms of star
2013-02-15 Ferruccio Guidiupdate in basic_2
2013-02-15 Ferruccio Guidiwe reformulate the extended computation to simplify...
2013-02-13 Ferruccio Guidistatistics update in basic_2
2013-02-13 Ferruccio Guidi- first piece of the mutual induction for preservation...
2013-02-11 Ferruccio Guidian update in basic_2
2013-02-11 Ferruccio Guidimore service lemmas in nat and lambdadelta
2013-02-07 Ferruccio Guidione table was nissing ...
2013-02-07 Ferruccio Guidiupdate in basic_2
2013-02-07 Ferruccio Guidieven more service lemmas ...
2013-02-07 Andrea AspertiA few integrations
2013-02-07 Andrea Aspertirestructuring
2013-02-07 Andrea Asperti(no commit message)
2013-02-07 Andrea Aspertirestructuring
2013-02-06 Ferruccio Guidiupdate in basic_2
2013-02-06 Ferruccio Guidi- lambdadelta: more service lemmas ...
2013-02-05 Ferruccio Guidisome missing files ...
2013-02-05 Claudio Sacerdoti... Bug fixed: .ml/.mli files were opened/closed even when...
2013-02-04 Claudio Sacerdoti... Bug fixed: "open X" were not printed in .mli because...
2013-02-04 Claudio Sacerdoti... Flushing needed before closing the channel.
2013-02-04 Claudio Sacerdoti... Improved exception handling.
2013-02-04 Claudio Sacerdoti... Bug fixed in pretty printing of mutual inductive types.
2013-02-04 Claudio Sacerdoti... Bug fixed: the indty can be typed with a Prod, not...
2013-02-04 Claudio Sacerdoti... New option -extract_ocaml to extract to ocaml files.
2013-02-04 Claudio Sacerdoti... Pretty printing of ocaml files slightly improved.
2013-02-04 Claudio Sacerdoti... Last known bug unrelated to names fixed: a fixpoint...
2013-02-04 Wilmer Ricciottistate mte2 renamed to mte_acc
2013-02-04 Claudio Sacerdoti... ...
2013-02-04 Wilmer Ricciotticonverting certain basic machines to composed machines
2013-02-04 Wilmer Ricciottidefs.ma was never really used
2013-02-02 Claudio Sacerdoti... Makefile to extract to ocaml code.
2013-02-02 Claudio Sacerdoti... Oops, part of last commit (ocaml extraction implementation)
2013-02-02 Claudio Sacerdoti... Ooops, this completes the previous commit (ocaml extrac...
2013-02-02 Claudio Sacerdoti... Implementation of Ocaml extraction (largely ported...
next