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

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

2008-05-02	Wilmer Ricciotti	Some destruct tactics got broken after last update...	commit \| commitdiff \| tree \| snapshot
2008-05-01	Claudio Sacerdoti...	More precise classification of failures.	commit \| commitdiff \| tree \| snapshot
2008-05-01	Claudio Sacerdoti...	List of all URIS comprising:	commit \| commitdiff \| tree \| snapshot
2008-05-01	Claudio Sacerdoti...	More options can now be set at the beginning of the...	commit \| commitdiff \| tree \| snapshot
2008-05-01	Claudio Sacerdoti...	Last (???) bug about variables with bodies fixed: we...	commit \| commitdiff \| tree \| snapshot
2008-05-01	Claudio Sacerdoti...	Another case where the presence of variables with bodie...	commit \| commitdiff \| tree \| snapshot
2008-05-01	Enrico Tassi	tagging 0.5.0-rc1	commit \| commitdiff \| tree \| snapshot
2008-05-01	Claudio Sacerdoti...	Bug fixed: application without arguments generated...	commit \| commitdiff \| tree \| snapshot
2008-05-01	Claudio Sacerdoti...	New bug found.	commit \| commitdiff \| tree \| snapshot
2008-04-30	Claudio Sacerdoti...	Things are getting better.	commit \| commitdiff \| tree \| snapshot
2008-04-30	Claudio Sacerdoti...	Implementation of guarded_by_destructor is now complete...	commit \| commitdiff \| tree \| snapshot
2008-04-30	Claudio Sacerdoti...	Reducing an open term should not be an error (or should...	commit \| commitdiff \| tree \| snapshot
2008-04-30	Claudio Sacerdoti...	stupid error fixed	commit \| commitdiff \| tree \| snapshot
2008-04-30	Claudio Sacerdoti...	fixed_args fixed to accept passing a partially applied...	commit \| commitdiff \| tree \| snapshot
2008-04-30	Enrico Tassi	added check on all bodies, only the one we actually...	commit \| commitdiff \| tree \| snapshot
2008-04-30	Enrico Tassi	added fake uri when the univ is anon	commit \| commitdiff \| tree \| snapshot
2008-04-30	Enrico Tassi	fixed wrong Rel, still to do: Fix(i,j) applied to dange...	commit \| commitdiff \| tree \| snapshot
2008-04-30	Enrico Tassi	universes are written with the URI inside objects,...	commit \| commitdiff \| tree \| snapshot
2008-04-30	Enrico Tassi	xml strict!	commit \| commitdiff \| tree \| snapshot
2008-04-30	Enrico Tassi	many pending modifications were there, now the website...	commit \| commitdiff \| tree \| snapshot
2008-04-30	Enrico Tassi	guarded_by_destructors on steroids	commit \| commitdiff \| tree \| snapshot
2008-04-30	Enrico Tassi	added list_mapi	commit \| commitdiff \| tree \| snapshot
2008-04-29	Claudio Sacerdoti...	Tests status update.	commit \| commitdiff \| tree \| snapshot
2008-04-29	Enrico Tassi	speedup in fixing the graph closures	commit \| commitdiff \| tree \| snapshot
2008-04-28	Claudio Sacerdoti...	Avoid (whd ~delta:true) during guarded_by_destructors...	commit \| commitdiff \| tree \| snapshot
2008-04-28	Claudio Sacerdoti...	In guarded by destructors, avoid computing the (whd...	commit \| commitdiff \| tree \| snapshot
2008-04-24	Claudio Sacerdoti...	Update...	commit \| commitdiff \| tree \| snapshot
2008-04-24	Claudio Sacerdoti...	No more bugs on guarded_by_constructors in the old...	commit \| commitdiff \| tree \| snapshot
2008-04-24	Claudio Sacerdoti...	When going under a binder, a term must be converted...	commit \| commitdiff \| tree \| snapshot
2008-04-24	Wilmer Ricciotti	Proof of adequacy.	commit \| commitdiff \| tree \| snapshot
2008-04-24	Enrico Tassi	guarded_by_constructor completely rewritten, fixed...	commit \| commitdiff \| tree \| snapshot
2008-04-24	Enrico Tassi	added coinductive example	commit \| commitdiff \| tree \| snapshot
2008-04-24	Claudio Sacerdoti...	Working and broken URIs.	commit \| commitdiff \| tree \| snapshot
2008-04-23	Enrico Tassi	ported the instantiate-left-params-to-calculate-rec...	commit \| commitdiff \| tree \| snapshot
2008-04-23	Claudio Sacerdoti...	Avoid other comparisons on universes using =.	commit \| commitdiff \| tree \| snapshot
2008-04-23	Claudio Sacerdoti...	Avoid code duplication.	commit \| commitdiff \| tree \| snapshot
2008-04-23	Claudio Sacerdoti...	Do NOT dare using Pervasives.compare on data structures...	commit \| commitdiff \| tree \| snapshot
2008-04-22	Enrico Tassi	oblivion ugraph everywhere outside the kernel	commit \| commitdiff \| tree \| snapshot
2008-04-22	Enrico Tassi	slow_implementation and some dead code removed	commit \| commitdiff \| tree \| snapshot
2008-04-22	Enrico Tassi	more strict check by CSC, I miss it	commit \| commitdiff \| tree \| snapshot
2008-04-22	Enrico Tassi	fix cache comparison relaxed to URI and not REFERENCE	commit \| commitdiff \| tree \| snapshot
2008-04-22	Enrico Tassi	added a call to ppcontext in the case of appl, to ease...	commit \| commitdiff \| tree \| snapshot
2008-04-22	Enrico Tassi	added ppcontext	commit \| commitdiff \| tree \| snapshot
2008-04-22	Claudio Sacerdoti...	Types for LetIns computed during parsing for Coq object...	commit \| commitdiff \| tree \| snapshot
2008-04-21	Claudio Sacerdoti...	defn2.ma is to be used with part1a_inversion3	commit \| commitdiff \| tree \| snapshot
2008-04-21	Enrico Tassi	fix universe handling, newly encountered objects are...	commit \| commitdiff \| tree \| snapshot
2008-04-20	Claudio Sacerdoti...	Alternative prove using just one induction/inversion...	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	better error message	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	impredicative set work around	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	impredicative set work around	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	associativity of -> fixed	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	ancient graph regarding universes and trust=false,...	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	extlib list_uniq instead of local copy	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	ranking function fixed: when graphs are collapsed one...	commit \| commitdiff \| tree \| snapshot
2008-04-19	Enrico Tassi	added flag to change Set into Type on the fly, that...	commit \| commitdiff \| tree \| snapshot
2008-04-19	Claudio Sacerdoti...	oblivion_ugraph => empty_ugraph	commit \| commitdiff \| tree \| snapshot
2008-04-19	Claudio Sacerdoti...	Added to flags to activate/disactivate pretty-printing...	commit \| commitdiff \| tree \| snapshot
2008-04-19	Claudio Sacerdoti...	Uris must be stripped of their xpointers.	commit \| commitdiff \| tree \| snapshot
2008-04-18	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree \| snapshot
2008-04-18	Claudio Sacerdoti...	Inversion lemma for Forall.	commit \| commitdiff \| tree \| snapshot
2008-04-18	Enrico Tassi	workaround for Pi associativity	commit \| commitdiff \| tree \| snapshot
2008-04-18	Enrico Tassi	workaround for some Set/Type problems	commit \| commitdiff \| tree \| snapshot
2008-04-18	Enrico Tassi	cicEnvironment refactoring with sound view of Coq`s...	commit \| commitdiff \| tree \| snapshot
2008-04-18	Enrico Tassi	assertion was wrong, an object can contain a named...	commit \| commitdiff \| tree \| snapshot
2008-04-18	Enrico Tassi	graph generation phase fixed	commit \| commitdiff \| tree \| snapshot
2008-04-18	Enrico Tassi	Appl case in is_really_smaller fixed as in the old...	commit \| commitdiff \| tree \| snapshot
2008-04-17	Enrico Tassi	example:	commit \| commitdiff \| tree \| snapshot
2008-04-17	Enrico Tassi	added a missing whd	commit \| commitdiff \| tree \| snapshot
2008-04-17	Enrico Tassi	new calculation of recursive parameters in guarded...	commit \| commitdiff \| tree \| snapshot
2008-04-17	Enrico Tassi	Two similar cases packed together	commit \| commitdiff \| tree \| snapshot
2008-04-17	Enrico Tassi	some fixes for guardness conditions	commit \| commitdiff \| tree \| snapshot
2008-04-17	Enrico Tassi	is_really_smaller in sync with old kernel, impossible...	commit \| commitdiff \| tree \| snapshot
2008-04-15	Claudio Sacerdoti...	check_is_really_smaller simplified to consider that...	commit \| commitdiff \| tree \| snapshot
2008-04-15	Claudio Sacerdoti...	1. bug fixed: the context must be type-checked before...	commit \| commitdiff \| tree \| snapshot
2008-04-15	Enrico Tassi	get_checked_fix -> get_checked_fixes	commit \| commitdiff \| tree \| snapshot
2008-04-15	Enrico Tassi	added comment	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom