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

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

2008-03-22	Enrico Tassi	freescale moved under contribs. contribs made relocatable	commit \| commitdiff \| tree \| snapshot
2008-03-20	Claudio Sacerdoti...	New syntax for auto-related tactics and conclude/obtain.	commit \| commitdiff \| tree \| snapshot
2008-03-20	Claudio Sacerdoti...	Script fixed (it did not compile due to a mistake befor...	commit \| commitdiff \| tree \| snapshot
2008-03-20	Ferruccio Guidi	Base-2 is not compiling properly and is excluded for now	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	changed auto_tac params type and all derivate tactics...	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	new semantics for 'by t'	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	removed pointless test	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	I believe that auto paramodulation does not try to	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	added library option to auto	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	letins are no more unfolded, we do that by hand	commit \| commitdiff \| tree \| snapshot
2008-03-20	Enrico Tassi	letin are no longer unfolded thus coercions not propaga...	commit \| commitdiff \| tree \| snapshot
2008-03-20	Claudio Sacerdoti...	End of patch for computation of LetIn types. Now types...	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	Bug: types and terms pushed into the context must be...	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	-debug improved	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	prerr_endline => debug_print	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	prerr_endline => debug_print	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	Number notation for Coq is back again, waiting for...	commit \| commitdiff \| tree \| snapshot
2008-03-19	Claudio Sacerdoti...	Files committed by Enrico (a mistake, I suppose) removed.	commit \| commitdiff \| tree \| snapshot
2008-03-19	Ferruccio Guidi	Procedural : added some missing cases	commit \| commitdiff \| tree \| snapshot
2008-03-18	Ferruccio Guidi	LAMBDA-TYPES: level 2 dependences are now correct,...	commit \| commitdiff \| tree \| snapshot
2008-03-18	Ferruccio Guidi	Procedural : tentative update to the new letin cic...	commit \| commitdiff \| tree \| snapshot
2008-03-14	Claudio Sacerdoti...	Tests enabled again.	commit \| commitdiff \| tree \| snapshot
2008-03-13	Claudio Sacerdoti...	:-(	commit \| commitdiff \| tree \| snapshot
2008-03-13	Claudio Sacerdoti...	New version of freescale:	commit \| commitdiff \| tree \| snapshot
2008-03-12	Claudio Sacerdoti...	Problem solved (was: apply needed an argument to avoid...	commit \| commitdiff \| tree \| snapshot
2008-03-12	Claudio Sacerdoti...	Almost always correct optimization: during unification...	commit \| commitdiff \| tree \| snapshot
2008-03-12	Enrico Tassi	fixed implicit	commit \| commitdiff \| tree \| snapshot
2008-03-12	Andrea Asperti	Nuova dimostrazione riflessiva di le_to_Bertrand.	commit \| commitdiff \| tree \| snapshot
2008-03-12	Enrico Tassi	if -debug is specified do not catch all exceptions	commit \| commitdiff \| tree \| snapshot
2008-03-11	Claudio Sacerdoti...	Very experimental commit: the type of the source is...	commit \| commitdiff \| tree \| snapshot
2008-03-10	Enrico Tassi	fixed wrong dependencies in debian package reported...	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	Bad hack to avoid failure of conversion (unfolding...	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	Scripts fixed because of:	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	Tactic reduce got rid of. Use normalize, instead.	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	whd: ~delta=false now controls also zeta-reduction...	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	An unimplemented case of clearbody is now implemented.	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	check_metasenv_consistency:	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	Example query fixed.	commit \| commitdiff \| tree \| snapshot
2008-03-10	Claudio Sacerdoti...	Debugging print removed.	commit \| commitdiff \| tree \| snapshot
2008-03-09	Claudio Sacerdoti...	Added ad-hoc optimization for check_metasenv_consistenc...	commit \| commitdiff \| tree \| snapshot
2008-03-09	Claudio Sacerdoti...	Performance improvement: let-ins should always be pushe...	commit \| commitdiff \| tree \| snapshot
2008-03-09	Claudio Sacerdoti...	Scripts fixed. They were broken since the change to...	commit \| commitdiff \| tree \| snapshot
2008-03-09	Ferruccio Guidi	LAMBDA-TYPES: some more generation lemmas and some...	commit \| commitdiff \| tree \| snapshot
2008-03-09	Claudio Sacerdoti...	Potentially (and, at least sometimes, actually) big...	commit \| commitdiff \| tree \| snapshot
2008-03-09	Claudio Sacerdoti...	Redundant check (because of an invariant) removed.	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	* please let the library in shape *	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	fixed	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	skipped freescale and dama_didactic	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	fixed deps	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	reworked freescale stuff to put \m as a left parameter	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	no more assembly/ to skip	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	fix typo	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	added mkdir	commit \| commitdiff \| tree \| snapshot
2008-03-06	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-03-05	Ferruccio Guidi	some corrections and additions	commit \| commitdiff \| tree \| snapshot
2008-03-05	Enrico Tassi	from now on, export MATITA_EXTRACT=true to extract	commit \| commitdiff \| tree \| snapshot
2008-03-05	Enrico Tassi	verbosity increased in case of error	commit \| commitdiff \| tree \| snapshot
2008-03-04	Ferruccio Guidi	components/library: dotdothack removed	commit \| commitdiff \| tree \| snapshot
2008-03-04	Claudio Sacerdoti...	New syntax for patterns.	commit \| commitdiff \| tree \| snapshot
2008-03-04	Claudio Sacerdoti...	prodT ==> prod	commit \| commitdiff \| tree \| snapshot
2008-03-04	Claudio Sacerdoti...	A) New version.	commit \| commitdiff \| tree \| snapshot
2008-02-29	Ferruccio Guidi	we added the classic substitution function	commit \| commitdiff \| tree \| snapshot
2008-02-28	Enrico Tassi	firs attempt to compile with ocamlbuild	commit \| commitdiff \| tree \| snapshot
2008-02-27	Wilmer Ricciotti	the proof of bertrand's conjecture is now complete	commit \| commitdiff \| tree \| snapshot
2008-02-26	Ferruccio Guidi	I added some debugging information	commit \| commitdiff \| tree \| snapshot
2008-02-26	Ferruccio Guidi	added MATITAOPTIONS -onepass as for LAMBDA-TYPES	commit \| commitdiff \| tree \| snapshot
2008-02-26	Ferruccio Guidi	LAMBDA-TYPES: added wf3 (legal context predicate);	commit \| commitdiff \| tree \| snapshot
2008-02-24	Ferruccio Guidi	$(H) added :)	commit \| commitdiff \| tree \| snapshot
2008-02-24	Ferruccio Guidi	LAMBDA-TYPES: dependences calculation improved	commit \| commitdiff \| tree \| snapshot
2008-02-23	Ferruccio Guidi	LAMBDA-TYPES:	commit \| commitdiff \| tree \| snapshot
2008-02-22	Ferruccio Guidi	- added some options to matitadep: -stdout and -exclude	commit \| commitdiff \| tree \| snapshot
2008-02-22	Wilmer Ricciotti	sieve of erathostene (proof of soundness almost done)	commit \| commitdiff \| tree \| snapshot
2008-02-21	Claudio Sacerdoti...	A new very simple example for recursive functions....	commit \| commitdiff \| tree \| snapshot
2008-02-21	Claudio Sacerdoti...	Avoid translating back recursive fixes to the same...	commit \| commitdiff \| tree \| snapshot
2008-02-21	Claudio Sacerdoti...	Avoid application to 0 arguments.	commit \| commitdiff \| tree \| snapshot
2008-02-21	Claudio Sacerdoti...	Better handling of exceptions.	commit \| commitdiff \| tree \| snapshot
2008-02-21	Ferruccio Guidi	svn:ignores fixed	commit \| commitdiff \| tree \| snapshot
2008-02-20	Ferruccio Guidi	-onepass option removed from Makefile to comile Base...	commit \| commitdiff \| tree \| snapshot
2008-02-20	Ferruccio Guidi	LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES	commit \| commitdiff \| tree \| snapshot
2008-02-20	Enrico Tassi	splat_args is now better understood and debugged: we...	commit \| commitdiff \| tree \| snapshot
2008-02-20	Enrico Tassi	added small test, fixed some bugs	commit \| commitdiff \| tree \| snapshot
2008-02-20	Enrico Tassi	many fixed in translation functions	commit \| commitdiff \| tree \| snapshot
2008-02-19	Ferruccio Guidi	dependences needed a fix :)	commit \| commitdiff \| tree \| snapshot
2008-02-19	Ferruccio Guidi	we are moving the devel root one dir level up	commit \| commitdiff \| tree \| snapshot
2008-02-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-02-19	Enrico Tassi	snapshot inverse tranformation	commit \| commitdiff \| tree \| snapshot
2008-02-19	Enrico Tassi	transformation almost finisced, not tested	commit \| commitdiff \| tree \| snapshot
2008-02-19	Ferruccio Guidi	now inline "file.ma" is allowed.	commit \| commitdiff \| tree \| snapshot
2008-02-19	Andrea Asperti	Added o.ma (some results about the magnitude of functio...	commit \| commitdiff \| tree \| snapshot
2008-02-19	Enrico Tassi	initial steps of convertibility	commit \| commitdiff \| tree \| snapshot
2008-02-18	Enrico Tassi	some bits of reduction, reusing psubst	commit \| commitdiff \| tree \| snapshot
2008-02-18	Andrea Asperti	Complete proof of Bertrand for n >= 256.	commit \| commitdiff \| tree \| snapshot
2008-02-14	Andrea Asperti	Prima versione di bertrand. Tanti cambiamenti qua e la.	commit \| commitdiff \| tree \| snapshot
2008-02-13	Ferruccio Guidi	baseuris removed from files	commit \| commitdiff \| tree \| snapshot
2008-02-13	Ferruccio Guidi	fixed dependences	commit \| commitdiff \| tree \| snapshot
2008-02-13	Enrico Tassi	conversion half inplemented	commit \| commitdiff \| tree \| snapshot
2008-02-13	Ferruccio Guidi	renaming	commit \| commitdiff \| tree \| snapshot
2008-02-13	Enrico Tassi	reordered cases	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom