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

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

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
2008-12-28	Claudio Sacerdoti...	o-algebra defined again	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	Categories and subsets compile again, hopefully with...	commit \| commitdiff \| tree \| snapshot
2008-12-28	Claudio Sacerdoti...	WARNING: partial commit to try to understand something.	commit \| commitdiff \| tree \| snapshot
2008-12-26	Claudio Sacerdoti...	Some more fixes. Boring and stupid!	commit \| commitdiff \| tree \| snapshot
2008-12-26	Claudio Sacerdoti...	Some fixes.	commit \| commitdiff \| tree \| snapshot
2008-12-26	Claudio Sacerdoti...	O-Basic Topologies do form a category.	commit \| commitdiff \| tree \| snapshot
2008-12-26	Claudio Sacerdoti...	A few more lines.	commit \| commitdiff \| tree \| snapshot
2008-12-26	Claudio Sacerdoti...	Some notes by Giovanni.	commit \| commitdiff \| tree \| snapshot
2008-12-26	Claudio Sacerdoti...	Some notes by Giovanni.	commit \| commitdiff \| tree \| snapshot
2008-12-24	Enrico Tassi	added some virtuals	commit \| commitdiff \| tree \| snapshot
2008-12-24	Enrico Tassi	bug fixed, all convertible was called without a metasenv	commit \| commitdiff \| tree \| snapshot
2008-12-22	Claudio Sacerdoti...	Just copied here from formal_topologies.ma.	commit \| commitdiff \| tree \| snapshot
2008-12-22	Claudio Sacerdoti...	More (ugly) work.	commit \| commitdiff \| tree \| snapshot
2008-12-22	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-22	Enrico Tassi	Beginning of o-basic_topologies.	commit \| commitdiff \| tree \| snapshot
2008-12-22	Enrico Tassi	Some clean up.	commit \| commitdiff \| tree \| snapshot
2008-12-22	Enrico Tassi	Concrete Spaces defined but... they require about 20m...	commit \| commitdiff \| tree \| snapshot
2008-12-22	Enrico Tassi	1 more lemma	commit \| commitdiff \| tree \| snapshot
2008-12-22	Enrico Tassi	one line	commit \| commitdiff \| tree \| snapshot
2008-12-22	Enrico Tassi	some work	commit \| commitdiff \| tree \| snapshot
2008-12-22	Claudio Sacerdoti...	ums got rid of	commit \| commitdiff \| tree \| snapshot
2008-12-21	Claudio Sacerdoti...	1) no more DAEMONS	commit \| commitdiff \| tree \| snapshot
2008-12-21	Enrico Tassi	merged commits, the same proof is missing :-(	commit \| commitdiff \| tree \| snapshot
2008-12-21	Enrico Tassi	bleah	commit \| commitdiff \| tree \| snapshot
2008-12-21	Claudio Sacerdoti...	Using the new category SET.	commit \| commitdiff \| tree \| snapshot
2008-12-21	Claudio Sacerdoti...	New category SET (whose objects are setoids).	commit \| commitdiff \| tree \| snapshot
2008-12-20	Ferruccio Guidi	we started the support for naive sort inclusion	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	better pp of virtuals	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	more pps	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	type3	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	ranking hopefully fixed	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	fix exponentiation	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	go notation go!	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	fixed, it seems the new handling of hints in some rare...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	added aliases for _ and fixed greek leters thanks to...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	better pps	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	handles bad Appl	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	added better debug_pps and add_user_provided_unificatio...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	added unification hint	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	unification hint	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	lambda case fixed, used to not properly use the expecte...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	added 'unification hint command to add a term to the...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	identity coercions are not really inserted, just used...	commit \| commitdiff \| tree \| snapshot
2008-12-19	Enrico Tassi	....	commit \| commitdiff \| tree \| snapshot
2008-12-18	Claudio Sacerdoti...	Stupid bug fixed: checkin the type in place of the...	commit \| commitdiff \| tree \| snapshot
2008-12-18	Claudio Sacerdoti...	New disambiguation commented out.	commit \| commitdiff \| tree \| snapshot
2008-12-18	Claudio Sacerdoti...	Many axioms are now proved... using many more (but...	commit \| commitdiff \| tree \| snapshot
2008-12-18	Claudio Sacerdoti...	Now it compiles again.	commit \| commitdiff \| tree \| snapshot
2008-12-18	Claudio Sacerdoti...	Refinement of axioms fixed. We did not check that the...	commit \| commitdiff \| tree \| snapshot
2008-12-18	Ferruccio Guidi	- improved logging	commit \| commitdiff \| tree \| snapshot
2008-12-18	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-17	Ferruccio Guidi	we started the support for the coercions "alle" and...	commit \| commitdiff \| tree \| snapshot
2008-12-17	Enrico Tassi	foo overlap	commit \| commitdiff \| tree \| snapshot
2008-12-17	Enrico Tassi	foo overlap	commit \| commitdiff \| tree \| snapshot
2008-12-17	Enrico Tassi	....	commit \| commitdiff \| tree \| snapshot
2008-12-16	Ferruccio Guidi	we added the implicit coercion for modus tollens	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	previous change was causing divergence	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	hints work better now	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	hints attached	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	removed debug code	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	fixed a bug, it used to report o wrong is_normal bit...	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	make it compile again	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	wrap object_not_found	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	move the printing in the right place	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	auto expansion of \tex macros added as a switch in...	commit \| commitdiff \| tree \| snapshot
2008-12-16	Enrico Tassi	added one asser	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	dep.opt regenerated	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	added unification hints	commit \| commitdiff \| tree \| snapshot
2008-12-15	Wilmer Ricciotti	Some changes to the pullback test, for debugging	commit \| commitdiff \| tree \| snapshot
2008-12-15	Wilmer Ricciotti	First attempt to implement unification hints.	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	use named types to force some constraints asap	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	To check if a term is type, do a whd of its sort before...	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	aded some whd, you should be able to declare something...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Claudio Sacerdoti...	The library is no longer automatically used during...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Ferruccio Guidi	- improved logging	commit \| commitdiff \| tree \| snapshot
2008-12-14	Ferruccio Guidi	new kernel basic_ag (with absolute local references)	commit \| commitdiff \| tree \| snapshot
2008-12-14	Ferruccio Guidi	we are changing the kernel version from basic_rg to...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Ferruccio Guidi	autItem : the uris of the objects involved in the impli...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom