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

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

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
2008-05-19	Enrico Tassi	renamed add_le_constraint to add_constraint since it...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Enrico Tassi	run fsub during night	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Bug fixed: when computing the left arguments, I was...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Enrico Tassi	names fixed accoding to the new ones generated after...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Enrico Tassi	revert last commit, context' -> context (added comment)	commit \| commitdiff \| tree \| snapshot
2008-05-18	Enrico Tassi	using the right names in the context to check match...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	New missing check implemented: the left parameters...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Dummy dependent products in inductive types arities...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	This commit avoids cleaning dummy dependent types in...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Implemented translation of inductive types from the...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Serious bug fixed: the max of two universes was compute...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Synch with the paper.	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	Error message improved.	commit \| commitdiff \| tree \| snapshot
2008-05-18	Claudio Sacerdoti...	More effective optimization: avoid introducing already...	commit \| commitdiff \| tree \| snapshot
2008-05-17	Enrico Tassi	impredicative Set is considered as Prop in the new...	commit \| commitdiff \| tree \| snapshot
2008-05-17	Claudio Sacerdoti...	New check implemented: the sort of each constructor...	commit \| commitdiff \| tree \| snapshot
2008-05-17	Claudio Sacerdoti...	Missing check implemented: the sort of each constructor...	commit \| commitdiff \| tree \| snapshot
2008-05-17	Claudio Sacerdoti...	The file bug_universi.ma shows a strage case where...	commit \| commitdiff \| tree \| snapshot
2008-05-17	Claudio Sacerdoti...	Missing whd.	commit \| commitdiff \| tree \| snapshot
2008-05-17	Claudio Sacerdoti...	Bug fixed: since circular <= graphs are allowed, added...	commit \| commitdiff \| tree \| snapshot
2008-05-17	Claudio Sacerdoti...	Bug fixed: only Type < Type1 was declared.	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom