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

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

2008-04-15	Claudio Sacerdoti...	added sample of guarded by in which coq is stronger	commit \| commitdiff \| tree \| snapshot
2008-04-15	Enrico Tassi	positivity check fixed, a MutInd not applied (but with...	commit \| commitdiff \| tree \| snapshot
2008-04-15	Enrico Tassi	do not use an implicit but a sort as a neutral term...	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	objects are typechecked to ensure there is a graph...	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	leftno should be increased of the expnamedsubst, but...	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	better error message	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	same_obj made more precise, fixed the order of the...	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	ficed fixpoint cache usage for mutual fix	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	fixed positivity conditions	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	added mk_fix i j r that given an r of a fix generated...	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	positivity condition was relying on the name declared...	commit \| commitdiff \| tree \| snapshot
2008-04-14	Enrico Tassi	added little optimization to not add twice the same arc	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	quinck and untested implementation of positivity condit...	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	added depndency of new kernel to metadata to allow...	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	FIXED bug, added assertion in case a universe inside...	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	added function to fresh types	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	call Unshare.fresh_types	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	load the graph of objects that depend on the ones reque...	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	use universe rank instead of Type0	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	Type related failures fixed	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	better pp of objects	commit \| commitdiff \| tree \| snapshot
2008-04-11	Claudio Sacerdoti...	Extracted code. The main executable is medium_tests...	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	removed useless file	commit \| commitdiff \| tree \| snapshot
2008-04-11	Enrico Tassi	fixed modules order	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom