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

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

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
2008-05-26	Ferruccio Guidi	better presentation of lambda-delta	commit \| commitdiff \| tree \| snapshot
2008-05-26	Ferruccio Guidi	- some bugs fixed in the domain-based preorders on...	commit \| commitdiff \| tree \| snapshot
2008-05-26	Enrico Tassi	added comment for zack	commit \| commitdiff \| tree \| snapshot
2008-05-26	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-26	Enrico Tassi	auto syntax updated	commit \| commitdiff \| tree \| snapshot
2008-05-26	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-24	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-05-24	Enrico Tassi	order of goals changes, open ones are preferred to...	commit \| commitdiff \| tree \| snapshot
2008-05-21	Enrico Tassi	minimal implementation of left parameters display	commit \| commitdiff \| tree \| snapshot
2008-05-21	Enrico Tassi	0.5.1 should be realased soon, the bug that was affecti...	commit \| commitdiff \| tree \| snapshot
2008-05-19	Claudio Sacerdoti...	Here is where we should add relevance checks.	commit \| commitdiff \| tree \| snapshot
2008-05-19	Claudio Sacerdoti...	Bug fixed in computation of leftnos: variables were...	commit \| commitdiff \| tree \| snapshot
2008-05-19	Claudio Sacerdoti...	Code simplification.	commit \| commitdiff \| tree \| snapshot
2008-05-19	Claudio Sacerdoti...	Added cprop <= type constraint.	commit \| commitdiff \| tree \| snapshot
2008-05-19	Claudio Sacerdoti...	We do not need to give cprop a special status yet.	commit \| commitdiff \| tree \| snapshot
2008-05-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-05-19	Claudio Sacerdoti...	CProp dropped in favour of a cprop universe exported...	commit \| commitdiff \| tree \| snapshot
2008-05-19	Enrico Tassi	added leftno to references f inductive types and constr...	commit \| commitdiff \| tree \| snapshot
2008-05-19	Enrico Tassi	added aps generation	commit \| commitdiff \| tree \| snapshot
2008-05-19	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom