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

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

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
2008-04-03	Enrico Tassi	debujin implemented with the map recursor	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	bug found rewriting the kernel backported: n instead...	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	non debruijned constructor may be useless elswere,...	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	guarded_by_destructor ported, many auxiliary functions...	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	removed FSF banner	commit \| commitdiff \| tree \| snapshot
2008-04-03	Enrico Tassi	added ugly test showing many many bugs in the current...	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	added slim version of does_not_occur	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	added translation of Set to Type0 (avoid warning)	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	fixes backported from the new kernel	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	removed dummy rewrite	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	removed dummy rewrite	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	removed dummy rewrites	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	fixed according to the new rewrite semantics (fails...	commit \| commitdiff \| tree \| snapshot
2008-04-02	Enrico Tassi	fixed depends after the removal of Fsub	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom