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

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

2009-02-01	Claudio Sacerdoti...	Towards fullness.	commit \| commitdiff \| tree \| snapshot
2009-02-01	Claudio Sacerdoti...	Renaming.	commit \| commitdiff \| tree \| snapshot
2009-02-01	Claudio Sacerdoti...	Renaming.	commit \| commitdiff \| tree \| snapshot
2009-01-30	Enrico Tassi	fix convertibility in case of application test_eq_only...	commit \| commitdiff \| tree \| snapshot
2009-01-29	Enrico Tassi	more polishing	commit \| commitdiff \| tree \| snapshot
2009-01-29	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-01-29	Enrico Tassi	application arguments are compared with test_eq_only...	commit \| commitdiff \| tree \| snapshot
2009-01-28	Enrico Tassi	some work	commit \| commitdiff \| tree \| snapshot
2009-01-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-01-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-01-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-01-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-01-27	Enrico Tassi	maction, mpadded and mstyle added to documentation	commit \| commitdiff \| tree \| snapshot
2009-01-26	Enrico Tassi	minor fixes	commit \| commitdiff \| tree \| snapshot
2009-01-26	Enrico Tassi	maction support added to notation, adopted for = AKA...	commit \| commitdiff \| tree \| snapshot
2009-01-26	Enrico Tassi	maction layout added to notation	commit \| commitdiff \| tree \| snapshot
2009-01-26	Enrico Tassi	we were generating a name for the main fix twice	commit \| commitdiff \| tree \| snapshot
2009-01-26	Enrico Tassi	added a number to identical error messages to ease...	commit \| commitdiff \| tree \| snapshot
2009-01-23	Ferruccio Guidi	OEIS sequence identifier found for P(n)	commit \| commitdiff \| tree \| snapshot
2009-01-22	Claudio Sacerdoti...	TODO	commit \| commitdiff \| tree \| snapshot
2009-01-21	Enrico Tassi	some minor fixes	commit \| commitdiff \| tree \| snapshot
2009-01-21	Enrico Tassi	a bit of work done while travelling to padova	commit \| commitdiff \| tree \| snapshot
2009-01-19	Enrico Tassi	- new notation.ma file with local and common notation	commit \| commitdiff \| tree \| snapshot
2009-01-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-01-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-01-19	Enrico Tassi	all pullbacks are attempted in sequence, removed many...	commit \| commitdiff \| tree \| snapshot
2009-01-18	Claudio Sacerdoti...	universe inconsistency fixed	commit \| commitdiff \| tree \| snapshot
2009-01-18	Claudio Sacerdoti...	SUBSETS_full up to universe inconsistency	commit \| commitdiff \| tree \| snapshot
2009-01-17	Claudio Sacerdoti...	faithful	commit \| commitdiff \| tree \| snapshot
2009-01-17	Claudio Sacerdoti...	CAT2	commit \| commitdiff \| tree \| snapshot
2009-01-16	Enrico Tassi	ceommented out metasenv	commit \| commitdiff \| tree \| snapshot
2009-01-16	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-01-16	Claudio Sacerdoti...	Sambin's result holds trivially since most of the field...	commit \| commitdiff \| tree \| snapshot
2009-01-16	Claudio Sacerdoti...	basic topologies are trivially o-basic topologies	commit \| commitdiff \| tree \| snapshot
2009-01-16	Claudio Sacerdoti...	1. new coercion(s) from CPropi to CProp	commit \| commitdiff \| tree \| snapshot
2009-01-15	Enrico Tassi	the new coercion behaviour (variants + composition...	commit \| commitdiff \| tree \| snapshot
2009-01-15	Enrico Tassi	added notation for 'Vdash	commit \| commitdiff \| tree \| snapshot
2009-01-15	Enrico Tassi	if the user attempts to insert a duplicate coercions...	commit \| commitdiff \| tree \| snapshot
2009-01-15	Enrico Tassi	unvariant also for coercions to funclass	commit \| commitdiff \| tree \| snapshot
2009-01-15	Enrico Tassi	- name mangling changed, added __ to separate additiona...	commit \| commitdiff \| tree \| snapshot
2009-01-15	Enrico Tassi	no more universe inconsistency printed to stderr	commit \| commitdiff \| tree \| snapshot
2009-01-15	Enrico Tassi	coercions that are marked as variant are unfolded when...	commit \| commitdiff \| tree \| snapshot
2009-01-15	Enrico Tassi	Coercions graph is printed between real types and not...	commit \| commitdiff \| tree \| snapshot
2009-01-14	Claudio Sacerdoti...	o_continous_relations are really o_relation_pair.....	commit \| commitdiff \| tree \| snapshot
2009-01-14	Claudio Sacerdoti...	o-basic_pairs are indeed examples of o-basic_topologies!	commit \| commitdiff \| tree \| snapshot
2009-01-13	Enrico Tassi	many changes regarding coercions:	commit \| commitdiff \| tree \| snapshot
2009-01-13	Claudio Sacerdoti...	- Added new output in standard C.	commit \| commitdiff \| tree \| snapshot
2009-01-12	Claudio Sacerdoti...	Some work on o-algebras towards the proof that a and...	commit \| commitdiff \| tree \| snapshot
2009-01-08	Claudio Sacerdoti...	The new coercion from SET to Type0 with higher priority...	commit \| commitdiff \| tree \| snapshot
2009-01-08	Enrico Tassi	more composites to make all happy!	commit \| commitdiff \| tree \| snapshot
2009-01-08	Enrico Tassi	eq over SET1 and SET no longer used	commit \| commitdiff \| tree \| snapshot
2009-01-08	Enrico Tassi	some more if/fi conversion due to the new . binding	commit \| commitdiff \| tree \| snapshot
2009-01-08	Enrico Tassi	unary_morphism_N : seoidN -> setoidN -> setoidN (was...	commit \| commitdiff \| tree \| snapshot
2009-01-08	Enrico Tassi	virtuals for () removed and bound to 'o'	commit \| commitdiff \| tree \| snapshot
2009-01-08	Claudio Sacerdoti...	Just a snapshot.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Enrico Tassi	coercions reordering implemented	commit \| commitdiff \| tree \| snapshot
2009-01-06	Enrico Tassi	updated	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	More work on concrete spaces.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Some work on concrete spaces.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Cool: only 8 universes in use.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	1) Some reorganization.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Some renaming to avoid confusion between saturations...	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Fixing universe levels for saturations and (partially...	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	The functor from BP to OBP has been defined (but no...	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Ok, even if not stated formally, now we know that the...	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	orelation_of_relation preserves equality and identities.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Basic pairs restored; require renaming to use them...	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Some progress: everything works well now.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Ooops, I forgot to commit this in the previous 3-4...	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	An hint moved to the right place.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	No more daemons, no more exTs.	commit \| commitdiff \| tree \| snapshot
2009-01-06	Claudio Sacerdoti...	Great: some significant progress in fixing universe...	commit \| commitdiff \| tree \| snapshot
2009-01-05	Enrico Tassi	removing (only from the interface) functions related...	commit \| commitdiff \| tree \| snapshot
2009-01-05	Enrico Tassi	added help on virtuals and UTF-8 equivalence classes	commit \| commitdiff \| tree \| snapshot
2009-01-05	Enrico Tassi	expand ligatures after \n too	commit \| commitdiff \| tree \| snapshot
2009-01-05	Enrico Tassi	added := -> \def	commit \| commitdiff \| tree \| snapshot
2009-01-05	Enrico Tassi	added some memory to virtuals eq classes	commit \| commitdiff \| tree \| snapshot
2009-01-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-01-04	Claudio Sacerdoti...	1. CProp_n fixed to be equal to Type_n to better unders...	commit \| commitdiff \| tree \| snapshot
2009-01-04	Claudio Sacerdoti...	Snapshot to try to understand something.	commit \| commitdiff \| tree \| snapshot
2009-01-04	Claudio Sacerdoti...	Some more progress, fighting universe inconsistencies.	commit \| commitdiff \| tree \| snapshot
2009-01-04	Claudio Sacerdoti...	Yet another universe problem :-(	commit \| commitdiff \| tree \| snapshot
2009-01-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-01-04	Claudio Sacerdoti...	Back to step 1: all files that used to pass now pass...	commit \| commitdiff \| tree \| snapshot
2009-01-04	Claudio Sacerdoti...	More re-organization.	commit \| commitdiff \| tree \| snapshot
2009-01-03	Claudio Sacerdoti...	Basic pairs went through with no problems.	commit \| commitdiff \| tree \| snapshot
2009-01-03	Claudio Sacerdoti...	Universe level fixed (litterally).	commit \| commitdiff \| tree \| snapshot
2009-01-03	Claudio Sacerdoti...	Niceness was just a temporary illusion :-(	commit \| commitdiff \| tree \| snapshot
2009-01-03	Claudio Sacerdoti...	Much, much nicer now.	commit \| commitdiff \| tree \| snapshot
2009-01-03	Claudio Sacerdoti...	Some more re-organization.	commit \| commitdiff \| tree \| snapshot
2009-01-03	Claudio Sacerdoti...	More re-working.	commit \| commitdiff \| tree \| snapshot
2009-01-03	Claudio Sacerdoti...	More reorganization.	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	equivalence_relations made uniform w.r.t. universe...	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	Final work for today.	commit \| commitdiff \| tree \| snapshot
2008-12-28	Enrico Tassi	removed duplicate notation	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	Some more painful work.	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	binary_meet is back again, with some effort	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	Many universe inconsistency avoided here and there.	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	The universe inconsistency comes from big union, that...	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	Proof that \Omega \sup A is an overlap algebra, up...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom