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

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

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
2008-05-17	Claudio Sacerdoti...	Bug fixed and further code semplification in management...	commit \| commitdiff \| tree \| snapshot
2008-05-17	Claudio Sacerdoti...	The code for universes was not correct in many borderli...	commit \| commitdiff \| tree \| snapshot
2008-05-16	Enrico Tassi	ranking reports the lest of univs	commit \| commitdiff \| tree \| snapshot
2008-05-16	Enrico Tassi	added new implementation of universes	commit \| commitdiff \| tree \| snapshot
2008-05-16	Enrico Tassi	added name_of_uri	commit \| commitdiff \| tree \| snapshot
2008-05-16	Enrico Tassi	meta VS meta in alpha_eq honors substitution	commit \| commitdiff \| tree \| snapshot
2008-05-16	Enrico Tassi	used ind/coind information in references	commit \| commitdiff \| tree \| snapshot
2008-05-16	Enrico Tassi	types where compared without lookig at test_eq_only	commit \| commitdiff \| tree \| snapshot
2008-05-15	Claudio Sacerdoti...	Timings	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	(Approximated) inference of relevance implemented:...	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	First implementation of irrelevance in conversion.	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	New function get_relevance and new (not exported) funct...	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	New function list_forall_default3. 3 euros to the first...	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	Bug fixed in computation of heights: a constant must...	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	Implementation of calculation of heights.	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	Typo fixed.	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	Major code semplification and bugs removed (thanks...	commit \| commitdiff \| tree \| snapshot
2008-05-15	Andrea Asperti	Removed two args from psubst.	commit \| commitdiff \| tree \| snapshot
2008-05-15	Enrico Tassi	height of constants properly handled	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	list_iter2_default_value moved to HExtlib. 1 euro to...	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	eat_lambdas and eat_or_subst_lambdas taken out of the...	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	debruijn simplified. It could go in nCicUtils, but...	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	Bug fixed: types were check for conversion in the wrong...	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	We forgot an important check: the declared and expected...	commit \| commitdiff \| tree \| snapshot
2008-05-14	Enrico Tassi	partial implementation of reduction up to a given height	commit \| commitdiff \| tree \| snapshot
2008-05-14	Enrico Tassi	fixed error message	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	New checks for well-formedness of metasenvs and substs.	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_...	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	Nicer graph.	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	map_hash moved to HExtlib	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	New function map_hash.	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	Generation of dot file.	commit \| commitdiff \| tree \| snapshot
2008-05-14	Claudio Sacerdoti...	New licence used uniformly everywhere.	commit \| commitdiff \| tree \| snapshot
2008-05-13	Ferruccio Guidi	we added a link to lambda-delta home page in the hope...	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	One more bug fixed: we tried to perform List.nth on...	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	More exceptions captured.	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	Bug fixed in pretty-printing of free Rels.	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	Never commit before trying to compile... stupid typo...	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	Used old kernel exception in place of brand new one.	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	- is_closed removed from the kernel (it used to make...	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	Library factorized out.	commit \| commitdiff \| tree \| snapshot
2008-05-13	Enrico Tassi	wrong test equality only fixed	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	Type of conjecture and subst_entry made uniform.	commit \| commitdiff \| tree \| snapshot
2008-05-13	Enrico Tassi	convertibility was taking a metasenv but not using it	commit \| commitdiff \| tree \| snapshot
2008-05-13	Claudio Sacerdoti...	Added boolean "is_inductive" to NReference.Ind	commit \| commitdiff \| tree \| snapshot
2008-05-12	Claudio Sacerdoti...	trust is always false by default	commit \| commitdiff \| tree \| snapshot
2008-05-12	Claudio Sacerdoti...	trust implemented, but in the nCicTypeChecker!	commit \| commitdiff \| tree \| snapshot
2008-05-12	Claudio Sacerdoti...	New implementation of CicEnvironment:	commit \| commitdiff \| tree \| snapshot
2008-05-12	Enrico Tassi	height is stored in the reference, no need to fetch...	commit \| commitdiff \| tree \| snapshot
2008-05-10	Enrico Tassi	fixed english	commit \| commitdiff \| tree \| snapshot
2008-05-10	Enrico Tassi	valid xml	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom