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

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

2008-06-20	Claudio Sacerdoti...	- partial implementation of pattern for case documented	commit \| commitdiff \| tree \| snapshot
2008-06-19	Enrico Tassi	fixed core notation	commit \| commitdiff \| tree \| snapshot
2008-06-19	Enrico Tassi	notation fixed to be NON associative by default	commit \| commitdiff \| tree \| snapshot
2008-06-19	Claudio Sacerdoti...	1. bug fixed in generalize_pattern: a lazy const_tac...	commit \| commitdiff \| tree \| snapshot
2008-06-19	Claudio Sacerdoti...	- notation fixed according to the new stricter semantics	commit \| commitdiff \| tree \| snapshot
2008-06-19	Ferruccio Guidi	- Procedural: we now check that an eliminator opens...	commit \| commitdiff \| tree \| snapshot
2008-06-19	Enrico Tassi	notation on steroids: 'term 40 x' is a valid variable...	commit \| commitdiff \| tree \| snapshot
2008-06-18	Claudio Sacerdoti...	interpretation documented	commit \| commitdiff \| tree \| snapshot
2008-06-18	Enrico Tassi	initial support for notation that specifies the precede...	commit \| commitdiff \| tree \| snapshot
2008-06-18	Enrico Tassi	removed unused variable	commit \| commitdiff \| tree \| snapshot
2008-06-18	Enrico Tassi	some work on Q	commit \| commitdiff \| tree \| snapshot
2008-06-17	Enrico Tassi	general reorganization and first (unconditional) proof...	commit \| commitdiff \| tree \| snapshot
2008-06-17	Enrico Tassi	reordering of lexicon status partially avoided to make...	commit \| commitdiff \| tree \| snapshot
2008-06-16	Ferruccio Guidi	transformation from automath to intermediate language...	commit \| commitdiff \| tree \| snapshot
2008-06-16	Enrico Tassi	Dedekind sigma completeness for the natural numbers.	commit \| commitdiff \| tree \| snapshot
2008-06-16	Enrico Tassi	typo	commit \| commitdiff \| tree \| snapshot
2008-06-13	Enrico Tassi	some notation added with a bit PITA	commit \| commitdiff \| tree \| snapshot
2008-06-13	Wilmer Ricciotti	final relevance check	commit \| commitdiff \| tree \| snapshot
2008-06-13	Ferruccio Guidi	copyright information added in the grundlagen text	commit \| commitdiff \| tree \| snapshot
2008-06-13	Enrico Tassi	when -debug do not catch	commit \| commitdiff \| tree \| snapshot
2008-06-13	Enrico Tassi	when -debug do not catch	commit \| commitdiff \| tree \| snapshot
2008-06-13	Enrico Tassi	replace assert false with AssertFailure	commit \| commitdiff \| tree \| snapshot
2008-06-13	Ferruccio Guidi	Initial version of the Helena Checker	commit \| commitdiff \| tree \| snapshot
2008-06-13	Claudio Sacerdoti...	New lemma	commit \| commitdiff \| tree \| snapshot
2008-06-13	Enrico Tassi	more notation	commit \| commitdiff \| tree \| snapshot
2008-06-13	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-06-13	Enrico Tassi	print the name not found in the env	commit \| commitdiff \| tree \| snapshot
2008-06-12	Enrico Tassi	Testing some performance tricks by caching the list...	commit \| commitdiff \| tree \| snapshot
2008-06-12	Enrico Tassi	better names in a lemma to increase readability	commit \| commitdiff \| tree \| snapshot
2008-06-12	Enrico Tassi	fixed some regressions	commit \| commitdiff \| tree \| snapshot
2008-06-11	Claudio Sacerdoti...	New, much faster implementation of factorize.	commit \| commitdiff \| tree \| snapshot
2008-06-11	Enrico Tassi	gran casino	commit \| commitdiff \| tree \| snapshot
2008-06-11	Enrico Tassi	meta not considered before in outtype	commit \| commitdiff \| tree \| snapshot
2008-06-10	Enrico Tassi	bla bla bla	commit \| commitdiff \| tree \| snapshot
2008-06-10	Wilmer Ricciotti	relevance check for Match	commit \| commitdiff \| tree \| snapshot
2008-06-10	Enrico Tassi	initial qork for models	commit \| commitdiff \| tree \| snapshot
2008-06-10	Wilmer Ricciotti	Added check of relevance lists for inductive types...	commit \| commitdiff \| tree \| snapshot
2008-06-10	Enrico Tassi	lebesgue proved	commit \| commitdiff \| tree \| snapshot
2008-06-10	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2008-06-09	Claudio Sacerdoti...	Most of the time, URIs can now be replaced with identif...	commit \| commitdiff \| tree \| snapshot
2008-06-09	Claudio Sacerdoti...	It is now possible to use identifiers in place of URI...	commit \| commitdiff \| tree \| snapshot
2008-06-09	Wilmer Ricciotti	Reverting to the previous version some files which...	commit \| commitdiff \| tree \| snapshot
2008-06-09	Wilmer Ricciotti	more proof irrelevance	commit \| commitdiff \| tree \| snapshot
2008-06-09	Enrico Tassi	initial work on lebesque	commit \| commitdiff \| tree \| snapshot
2008-06-09	Enrico Tassi	exhaustivity completed	commit \| commitdiff \| tree \| snapshot
2008-06-09	Enrico Tassi	exhaustivity, some work	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	generalize no more required by elim	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	Generalize no more required for elim.	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	generalize no more useful for elim	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	Bug fixed: wrong default pattern for generalize.	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	New: pattern for elim documented.	commit \| commitdiff \| tree \| snapshot
2008-06-08	Claudio Sacerdoti...	Hypotheses patterns for elim implemented. No more need...	commit \| commitdiff \| tree \| snapshot
2008-06-07	Enrico Tassi	exhaustivity defined	commit \| commitdiff \| tree \| snapshot
2008-06-07	Enrico Tassi	proof simplified	commit \| commitdiff \| tree \| snapshot
2008-06-06	Claudio Sacerdoti...	Even more Q stuff moved around.	commit \| commitdiff \| tree \| snapshot
2008-06-06	Claudio Sacerdoti...	Even more Q stuff classified.	commit \| commitdiff \| tree \| snapshot
2008-06-06	Enrico Tassi	lemma 3.6 subverted	commit \| commitdiff \| tree \| snapshot
2008-06-06	Claudio Sacerdoti...	more stuff moved around	commit \| commitdiff \| tree \| snapshot
2008-06-06	Claudio Sacerdoti...	More Q stuff organized in a coherent way.	commit \| commitdiff \| tree \| snapshot
2008-06-06	Claudio Sacerdoti...	First snapshot at trying to clean up the Q library.	commit \| commitdiff \| tree \| snapshot
2008-06-06	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-06-06	Andrea Asperti	A new theorem	commit \| commitdiff \| tree \| snapshot
2008-06-06	Andrea Asperti	cleanup	commit \| commitdiff \| tree \| snapshot
2008-06-06	Andrea Asperti	Cleanup.	commit \| commitdiff \| tree \| snapshot
2008-06-06	Claudio Sacerdoti...	sieve.ma now depends only on primes.ma	commit \| commitdiff \| tree \| snapshot
2008-06-06	Andrea Asperti	Added frac.ma	commit \| commitdiff \| tree \| snapshot
2008-06-06	Andrea Asperti	Added Qplus_andrea.ma	commit \| commitdiff \| tree \| snapshot
2008-06-06	Claudio Sacerdoti...	Reduce reduction tactic got rid of a long time ago.	commit \| commitdiff \| tree \| snapshot
2008-06-05	Claudio Sacerdoti...	Eratosthene's sieve factorized out of nat/bertrand...	commit \| commitdiff \| tree \| snapshot
2008-06-05	Enrico Tassi	....	commit \| commitdiff \| tree \| snapshot
2008-06-05	Enrico Tassi	added order_continuity	commit \| commitdiff \| tree \| snapshot
2008-06-05	Enrico Tassi	sandwich is back	commit \| commitdiff \| tree \| snapshot
2008-06-04	Wilmer Ricciotti	Proof-irrelevance check for all applications (first...	commit \| commitdiff \| tree \| snapshot
2008-06-04	Wilmer Ricciotti	incomplete irrelevance test commented out	commit \| commitdiff \| tree \| snapshot
2008-06-03	Claudio Sacerdoti...	Some proofs on enumerator and denominator.	commit \| commitdiff \| tree \| snapshot
2008-06-03	Claudio Sacerdoti...	More work on rational numbers with unique representations.	commit \| commitdiff \| tree \| snapshot
2008-06-03	Enrico Tassi	some work on uniformity	commit \| commitdiff \| tree \| snapshot
2008-06-03	Enrico Tassi	end of section 2.2	commit \| commitdiff \| tree \| snapshot
2008-06-03	Enrico Tassi	proof refactored	commit \| commitdiff \| tree \| snapshot
2008-06-03	Enrico Tassi	xxx	commit \| commitdiff \| tree \| snapshot
2008-06-01	Enrico Tassi	more work on supremum	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	CProp hierarchy is there!	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	irrelevance check half implemented but already impossib...	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	garbage removed	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	more work on dama	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	prod moved under lambda-prolog unification case	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	added CProp	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	thanks to the fact that we convert well typed term...	commit \| commitdiff \| tree \| snapshot
2008-05-30	Enrico Tassi	added a bit more reduction in case Prod v.s. term,...	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	relevance check partially implemented but bugged since...	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	case not unfilding fixed	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	CProp, since it was defined in CoRN as a Type, is predi...	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	0.5.1 released	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	unused variables removed	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom