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

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

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
2008-05-29	Enrico Tassi	ref sync check fixed controlling fix/cofix coherence	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	first page of the new dama proof	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-29	Enrico Tassi	the type of the match was obtained reducing the outtype	commit \| commitdiff \| tree \| snapshot
2008-05-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-28	Enrico Tassi	dama restarted	commit \| commitdiff \| tree \| snapshot
2008-05-28	Enrico Tassi	cleanup	commit \| commitdiff \| tree \| snapshot
2008-05-28	Enrico Tassi	the attempt of completing dama using duality frozen	commit \| commitdiff \| tree \| snapshot
2008-05-28	Enrico Tassi	0.5.1	commit \| commitdiff \| tree \| snapshot
2008-05-27	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-27	Enrico Tassi	smarter lexer needed by lambda-delta that is splitting...	commit \| commitdiff \| tree \| snapshot
2008-05-27	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-27	Enrico Tassi	CoRN moved in contribs	commit \| commitdiff \| tree \| snapshot
2008-05-27	Enrico Tassi	frst step to move away the CoRN stuff	commit \| commitdiff \| tree \| snapshot
2008-05-27	Enrico Tassi	frst step to move away the CoRN stuff	commit \| commitdiff \| tree \| snapshot
2008-05-27	Enrico Tassi	auto calls cleanup\	commit \| commitdiff \| tree \| snapshot
2008-05-26	Enrico Tassi	better description of declarative tactics	commit \| commitdiff \| tree \| snapshot
2008-05-26	Enrico Tassi	new, more rigid syntax, for auto_params affecting the...	commit \| commitdiff \| tree \| snapshot
2008-05-26	Enrico Tassi	Universe.key was not used to index terms, but was used...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom