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

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

2008-04-01	Enrico Tassi	progress made better, still not perfect	commit \| commitdiff \| tree \| snapshot
2008-04-01	Enrico Tassi	added to rewrite a check to effectively do something...	commit \| commitdiff \| tree \| snapshot
2008-04-01	Enrico Tassi	added some comments, but the samentics of many function...	commit \| commitdiff \| tree \| snapshot
2008-04-01	Enrico Tassi	added set_ppterm	commit \| commitdiff \| tree \| snapshot
2008-03-31	Claudio Sacerdoti...	Automatic generation of elimination and inversion princ...	commit \| commitdiff \| tree \| snapshot
2008-03-31	Claudio Sacerdoti...	Large amount of duplicated code (still in comments...	commit \| commitdiff \| tree \| snapshot
2008-03-31	Claudio Sacerdoti...	1) Impredicative sort "Set" removed everywhere.	commit \| commitdiff \| tree \| snapshot
2008-03-31	Claudio Sacerdoti...	1) more sharing everywhere in NCicSubstitution	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	more cases of the type checker honoured, still missing...	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	added is_closed to nCicUtils.	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	moved psubst and list to the new iterators, result...	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	added iterators over NCic terms	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	removed FSF header	commit \| commitdiff \| tree \| snapshot
2008-03-27	Wilmer Ricciotti	Updated depedencies.	commit \| commitdiff \| tree \| snapshot
2008-03-27	Enrico Tassi	insert comments of old tpechecker	commit \| commitdiff \| tree \| snapshot
2008-03-26	Wilmer Ricciotti	Reorganization of list library (step 1)	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	new are_convertible and head_beta_reduce	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	context for fixpoint body created in the hopefully...	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	ported to the Cic LetIn with explicit type	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	this patch is a shit, the part that fixes the heuristic...	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	fix with m (to be optimized) are rewritten such that...	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	very very interesting hack	commit \| commitdiff \| tree \| snapshot
2008-03-25	Wilmer Ricciotti	small update	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	argument of type mcu_type always abstracted first	commit \| commitdiff \| tree \| snapshot
2008-03-25	Enrico Tassi	XXX this is the beginning of the metaocaml work XXX	commit \| commitdiff \| tree \| snapshot
2008-03-23	Enrico Tassi	Fsub moved in contribs	commit \| commitdiff \| tree \| snapshot
2008-03-23	Ferruccio Guidi	cicNotationPp: fixed letin syntax (now typeless)	commit \| commitdiff \| tree \| snapshot
2008-03-22	Enrico Tassi	since many stuff is under contrib, we need to ignore...	commit \| commitdiff \| tree \| snapshot
2008-03-22	Enrico Tassi	library_auto moved inside contrib, still not ported...	commit \| commitdiff \| tree \| snapshot
2008-03-22	Enrico Tassi	moved dama/ and dama_didactic/ in contribs/dama/	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom