matita.cs.unibo.it Git - helm.git/shortlog

]> matita.cs.unibo.it Git - helm.git/shortlog

2013-03-11	Andrea Asperti	Chpater 4 and 5	commit \| commitdiff \| tree \| snapshot
2013-03-10	Ferruccio Guidi	- improved Makefile esp. with the "trim" function	commit \| commitdiff \| tree \| snapshot
2013-03-10	Andrea Asperti	chapters 2 e 3	commit \| commitdiff \| tree \| snapshot
2013-03-10	Ferruccio Guidi	we removed a useless assertion that was forcing matita...	commit \| commitdiff \| tree \| snapshot
2013-03-09	Ferruccio Guidi	- update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-03-09	Ferruccio Guidi	basic_2_src.tbl was not updated :(	commit \| commitdiff \| tree \| snapshot
2013-03-09	Ferruccio Guidi	- lenv refinement for stratified native validity redefined	commit \| commitdiff \| tree \| snapshot
2013-03-08	Ferruccio Guidi	second recursive part of preservation finally proved!	commit \| commitdiff \| tree \| snapshot
2013-03-08	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-03-08	Ferruccio Guidi	improved "big treee" computation allows to close a...	commit \| commitdiff \| tree \| snapshot
2013-03-04	Claudio Sacerdoti...	Bug fixed: let-rec defined propositions are no longer...	commit \| commitdiff \| tree \| snapshot
2013-03-03	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-03-03	Ferruccio Guidi	- lambdadelta: we removed focalized reduction from...	commit \| commitdiff \| tree \| snapshot
2013-02-28	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-02-28	Ferruccio Guidi	- lambdadelta: first recursive part of preservation...	commit \| commitdiff \| tree \| snapshot
2013-02-28	Andrea Asperti	chapter2 revisited	commit \| commitdiff \| tree \| snapshot
2013-02-27	Claudio Sacerdoti...	Quick patch: the maxmeta is now pushed/popped when...	commit \| commitdiff \| tree \| snapshot
2013-02-27	Claudio Sacerdoti...	Quick patch: the maxmeta is now pushed/popped when...	commit \| commitdiff \| tree \| snapshot
2013-02-27	Claudio Sacerdoti...	Bug fixed: composite coercions were not extracted.	commit \| commitdiff \| tree \| snapshot
2013-02-27	Claudio Sacerdoti...	Bug fixed that reveals a new one: in case of inductive...	commit \| commitdiff \| tree \| snapshot
2013-02-27	Claudio Sacerdoti...	Ferruccio's removal of objects commented out because...	commit \| commitdiff \| tree \| snapshot
2013-02-27	Andrea Asperti	Chapter 1 revisited	commit \| commitdiff \| tree \| snapshot
2013-02-25	Ferruccio Guidi	when we serialize the contents of a .ma, we remove...	commit \| commitdiff \| tree \| snapshot
2013-02-24	Ferruccio Guidi	- xhtbl: now double quotes can appear in string literals	commit \| commitdiff \| tree \| snapshot
2013-02-24	Ferruccio Guidi	- nUri : added Sets of uris for use in "probe"	commit \| commitdiff \| tree \| snapshot
2013-02-22	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-02-22	Ferruccio Guidi	- "big tree" order implemented	commit \| commitdiff \| tree \| snapshot
2013-02-18	Ferruccio Guidi	trace added in a failing invocation of auto :-(	commit \| commitdiff \| tree \| snapshot
2013-02-18	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-02-18	Ferruccio Guidi	substitution lemma for stratified native validity!	commit \| commitdiff \| tree \| snapshot
2013-02-15	Ferruccio Guidi	update in basic_2 summary	commit \| commitdiff \| tree \| snapshot
2013-02-15	Ferruccio Guidi	we rephrased sstas in terms of star	commit \| commitdiff \| tree \| snapshot
2013-02-15	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-02-15	Ferruccio Guidi	we reformulate the extended computation to simplify...	commit \| commitdiff \| tree \| snapshot
2013-02-13	Ferruccio Guidi	statistics update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-02-13	Ferruccio Guidi	- first piece of the mutual induction for preservation...	commit \| commitdiff \| tree \| snapshot
2013-02-11	Ferruccio Guidi	an update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-02-11	Ferruccio Guidi	more service lemmas in nat and lambdadelta	commit \| commitdiff \| tree \| snapshot
2013-02-07	Ferruccio Guidi	one table was nissing ...	commit \| commitdiff \| tree \| snapshot
2013-02-07	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-02-07	Ferruccio Guidi	even more service lemmas ...	commit \| commitdiff \| tree \| snapshot
2013-02-07	Andrea Asperti	A few integrations	commit \| commitdiff \| tree \| snapshot
2013-02-07	Andrea Asperti	restructuring	commit \| commitdiff \| tree \| snapshot
2013-02-07	Andrea Asperti	(no commit message)	commit \| commitdiff \| tree \| snapshot
2013-02-07	Andrea Asperti	restructuring	commit \| commitdiff \| tree \| snapshot
2013-02-06	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-02-06	Ferruccio Guidi	- lambdadelta: more service lemmas ...	commit \| commitdiff \| tree \| snapshot
2013-02-05	Ferruccio Guidi	some missing files ...	commit \| commitdiff \| tree \| snapshot
2013-02-05	Claudio Sacerdoti...	Bug fixed: .ml/.mli files were opened/closed even when...	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	Bug fixed: "open X" were not printed in .mli because...	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	Flushing needed before closing the channel.	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	Improved exception handling.	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	Bug fixed in pretty printing of mutual inductive types.	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	Bug fixed: the indty can be typed with a Prod, not...	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	New option -extract_ocaml to extract to ocaml files.	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	Pretty printing of ocaml files slightly improved.	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	Last known bug unrelated to names fixed: a fixpoint...	commit \| commitdiff \| tree \| snapshot
2013-02-04	Wilmer Ricciotti	state mte2 renamed to mte_acc	commit \| commitdiff \| tree \| snapshot
2013-02-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2013-02-04	Wilmer Ricciotti	converting certain basic machines to composed machines	commit \| commitdiff \| tree \| snapshot
2013-02-04	Wilmer Ricciotti	defs.ma was never really used	commit \| commitdiff \| tree \| snapshot
2013-02-02	Claudio Sacerdoti...	Makefile to extract to ocaml code.	commit \| commitdiff \| tree \| snapshot
2013-02-02	Claudio Sacerdoti...	Oops, part of last commit (ocaml extraction implementation)	commit \| commitdiff \| tree \| snapshot
2013-02-02	Claudio Sacerdoti...	Ooops, this completes the previous commit (ocaml extrac...	commit \| commitdiff \| tree \| snapshot
2013-02-02	Claudio Sacerdoti...	Implementation of Ocaml extraction (largely ported...	commit \| commitdiff \| tree \| snapshot
2013-02-02	Claudio Sacerdoti...	Identity change, improves readability.	commit \| commitdiff \| tree \| snapshot
2013-02-01	Ferruccio Guidi	- Now the nodes count does not include the generated...	commit \| commitdiff \| tree \| snapshot
2013-02-01	Ferruccio Guidi	lambda finaly moved in lib	commit \| commitdiff \| tree \| snapshot
2013-02-01	Wilmer Ricciotti	match now only uses the new move operation	commit \| commitdiff \| tree \| snapshot
2013-02-01	Ferruccio Guidi	- ng_refiner:	commit \| commitdiff \| tree \| snapshot
2013-01-29	Wilmer Ricciotti	Speed-up in match.ma.	commit \| commitdiff \| tree \| snapshot
2013-01-29	Wilmer Ricciotti	Proved old axiom.	commit \| commitdiff \| tree \| snapshot
2013-01-29	Wilmer Ricciotti	Yippeee! Completes proof of soundness of the universal...	commit \| commitdiff \| tree \| snapshot
2013-01-28	Andrea Asperti	unistep!!!	commit \| commitdiff \| tree \| snapshot
2013-01-28	Ferruccio Guidi	update in basic_2	commit \| commitdiff \| tree \| snapshot
2013-01-28	Ferruccio Guidi	- notation change for weight functions (following lambda)	commit \| commitdiff \| tree \| snapshot
2013-01-28	Andrea Asperti	funzioni ausiliarie	commit \| commitdiff \| tree \| snapshot
2013-01-28	Wilmer Ricciotti	cfg_in_table_to_tuple	commit \| commitdiff \| tree \| snapshot
2013-01-28	Wilmer Ricciotti	sem_copy_strict	commit \| commitdiff \| tree \| snapshot
2013-01-27	Wilmer Ricciotti	many axioms and daemons removed	commit \| commitdiff \| tree \| snapshot
2013-01-27	Andrea Asperti	quasi finito	commit \| commitdiff \| tree \| snapshot
2013-01-27	Wilmer Ricciotti	well-foundedness done	commit \| commitdiff \| tree \| snapshot
2013-01-27	Andrea Asperti	sem_exec_move completed	commit \| commitdiff \| tree \| snapshot
2013-01-27	Andrea Asperti	almost there	commit \| commitdiff \| tree \| snapshot
2013-01-26	Andrea Asperti	A lot of changes	commit \| commitdiff \| tree \| snapshot
2013-01-25	Andrea Asperti	Splitted unistep_aux	commit \| commitdiff \| tree \| snapshot
2013-01-25	Wilmer Ricciotti	started unistep	commit \| commitdiff \| tree \| snapshot
2013-01-25	Wilmer Ricciotti	progress in termination	commit \| commitdiff \| tree \| snapshot
2013-01-25	Ferruccio Guidi	- paths and left residuals: forth case of the equivalen...	commit \| commitdiff \| tree \| snapshot
2013-01-24	Wilmer Ricciotti	finished semantics for termination of match machine	commit \| commitdiff \| tree \| snapshot
2013-01-24	Wilmer Ricciotti	progress	commit \| commitdiff \| tree \| snapshot
2013-01-24	Wilmer Ricciotti	progress	commit \| commitdiff \| tree \| snapshot
2013-01-23	Ferruccio Guidi	- paths and left residuals: third case of the equivalen...	commit \| commitdiff \| tree \| snapshot
2013-01-23	Wilmer Ricciotti	progress	commit \| commitdiff \| tree \| snapshot
2013-01-22	Andrea Asperti	termination!	commit \| commitdiff \| tree \| snapshot
2013-01-22	Andrea Asperti	Universal machine	commit \| commitdiff \| tree \| snapshot
2013-01-22	Wilmer Ricciotti	Removed all axioms in unistep_aux	commit \| commitdiff \| tree \| snapshot
2013-01-21	Wilmer Ricciotti	removed daemons	commit \| commitdiff \| tree \| snapshot
2013-01-21	Andrea Asperti	universal	commit \| commitdiff \| tree \| snapshot
2013-01-21	Wilmer Ricciotti	tape_move_obj completed (modulo daemons)	commit \| commitdiff \| tree \| snapshot
next

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom