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

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

2008-04-11	Enrico Tassi	more fix removed from types	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	more fix removed from types in proofs	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	when we build the elimination principle we fresh univer...	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	added a parameter to unshare universes	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	Conversion of 2 lambdas was not requiring equality...	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	context of types built in the reverse order	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	added a simplify to prevent the generation of an ugly fix	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	implemented inductive and less parentheses	commit \| commitdiff \| tree \| snapshot
2008-04-10	Claudio Sacerdoti...	The cache of objects is now used also for cofixpoints.	commit \| commitdiff \| tree \| snapshot
2008-04-10	Claudio Sacerdoti...	New: cache of translated fixpoints (to avoid the genera...	commit \| commitdiff \| tree \| snapshot
2008-04-10	Claudio Sacerdoti...	does_not_occur exported to be used in oCic2NCic	commit \| commitdiff \| tree \| snapshot
2008-04-09	Claudio Sacerdoti...	Bug fixed: references to CoFix are CoFix, not Fix.	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	print unnamed variables as __n	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	switch off profilers	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	pp with parenthesis only when necessary and with some...	commit \| commitdiff \| tree \| snapshot
2008-04-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-04-09	Claudio Sacerdoti...	Fixed serious bug that occurred only in the following...	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	better pp in Appl	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	better pp	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	pretty printer on steroids	commit \| commitdiff \| tree \| snapshot
2008-04-09	Claudio Sacerdoti...	Added some "\n" here and there to the pretty-printing...	commit \| commitdiff \| tree \| snapshot
2008-04-09	Claudio Sacerdoti...	Grave bug fixed: Ce that point to definitions were...	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	added profiling on/off	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	invalidate fixed	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	allow to switch profiling on and off on the fly	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	removed two useless calls to the environment, one still...	commit \| commitdiff \| tree \| snapshot
2008-04-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Variables are no longer experted (cooking is now implem...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Swapped arguments in error message.	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Variables having a body can occur in cooked terms and...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Fix over the previous one: Var-LetIn abstractions shoul...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Error message improved.	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Cooking w.r.t. variables with bodies is now implemented...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Fix name capture in cofix.	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	To test the translation.	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Name capture fixed.	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Improved error messages in place of "sort elimination...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Seed reset before each convert_obj.	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Use seed to avoid further name clashes.	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Incredible, but true! Our name mangling clashed with...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Cooked objects are no longer well typed in the uncooked...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Improved eat_prods error message (at the cost of passin...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	The old kernel does not accept ens whose order is diffe...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Bad alpha-conversion by Enrico fixed.	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	Bug fixed: the ens need not be ordered w.r.t. the decla...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	j off by one in error message	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	fix_outty partially fixed: missing lifts in args and ens	commit \| commitdiff \| tree \| snapshot
2008-04-08	Claudio Sacerdoti...	fix_outty fixed in order to perform eta-expansion when...	commit \| commitdiff \| tree \| snapshot
2008-04-08	Enrico Tassi	added simplify to avoid ugly proofterm	commit \| commitdiff \| tree \| snapshot
2008-04-07	Claudio Sacerdoti...	Tentative (and bad!) fix of outtypes in non-dependent...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Claudio Sacerdoti...	Cooking discriminated into cooking in types (using...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Claudio Sacerdoti...	Pretty-printing of definitions fixed.	commit \| commitdiff \| tree \| snapshot
2008-04-07	Claudio Sacerdoti...	Cooking implemented (not tested yet).	commit \| commitdiff \| tree \| snapshot
2008-04-07	Claudio Sacerdoti...	Reports improved.	commit \| commitdiff \| tree \| snapshot
2008-04-07	Claudio Sacerdoti...	Debugging code fixed.	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added invalidate to clear the cache and ease the compar...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	commented out uris of objs that do not compile properly	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added comparison with old kernel	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	fixed error message for eat prods	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	invalidate	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	uris relative to axioms are translated in the right way	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added invalidate	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added preliminary checks for indtys	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	call get_obj instead of get_cooked_obj ~trust:false	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added case of const and axiom	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added # to comment	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	better printings	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	the explicit type in a LetIn must be typecheckd before...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	opt compilation enabled, removed some pps, check has...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	lefts_ad_tys properly sorted, added some metasenv here...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	lefts_and_tys was tys@lefts, CSC claims it was working...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added a list of uris to ease debugging	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	print the excpetion and raise it again, seems to produc...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	new constants have depth = max_int insted of 0 so that...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	off by one in calling count_from	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	fixed bug in translating Fix, recno was not properly...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	added a pretty printing of the new object and use argv...	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	context, metasenv and subst made mandatory in CicPp	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	guarded by has a nice error message	commit \| commitdiff \| tree \| snapshot
2008-04-07	Enrico Tassi	reference type made private, added mk_constructor to...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	some debug printings	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added to the cache a boolean to state if the object is	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	fix	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	today it seems that the substituted should be lifted...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added ppobj	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	type_of_constant was retunrning the type of the wrong...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	fixed list.nth and added some paretheses	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added some printings and catched more exceptions	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	removed useless printing	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	iterator map was mapping Lambdas to Prods!!!	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	debugging started	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	type of constant ported	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added add_obj to store objects in the environment,...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	logger added	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	added get_obj in nCicEnvironment that returns an object...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	indentation fixed	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	returns_a_counductive implemented	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	type_of_branch ported and optimized to not lift the...	commit \| commitdiff \| tree \| snapshot
2008-04-04	Enrico Tassi	is_really_smaller ported, still to understand the case...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom