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

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

2009-08-04	Cosimo Oliboni	freescle porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-04	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-03	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-01	Claudio Sacerdoti...	Smaller formulae.	commit \| commitdiff \| tree \| snapshot
2009-08-01	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-31	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-31	Claudio Sacerdoti...	Setoids, setoids1, sets, and the like. The mess begins.	commit \| commitdiff \| tree \| snapshot
2009-07-31	Claudio Sacerdoti...	Bad patch reverted (in error message).	commit \| commitdiff \| tree \| snapshot
2009-07-31	Claudio Sacerdoti...	Bug fixed: one case of too many arguments was not detec...	commit \| commitdiff \| tree \| snapshot
2009-07-31	Claudio Sacerdoti...	Serious bug fixed: uris were not refreshed when loading...	commit \| commitdiff \| tree \| snapshot
2009-07-31	Claudio Sacerdoti...	Record projections are now defined as fixpoints in...	commit \| commitdiff \| tree \| snapshot
2009-07-31	Claudio Sacerdoti...	\ldots are now used in nelim and ncases	commit \| commitdiff \| tree \| snapshot
2009-07-31	Claudio Sacerdoti...	Pp fixed in order to obtain read-back.	commit \| commitdiff \| tree \| snapshot
2009-07-30	Claudio Sacerdoti...	1) \ldots here and there	commit \| commitdiff \| tree \| snapshot
2009-07-30	Claudio Sacerdoti...	More napply \ldots => napply	commit \| commitdiff \| tree \| snapshot
2009-07-30	Claudio Sacerdoti...	napply now automatically inserts \ldots at the end	commit \| commitdiff \| tree \| snapshot
2009-07-30	Claudio Sacerdoti...	More \ldots.	commit \| commitdiff \| tree \| snapshot
2009-07-30	Claudio Sacerdoti...	\ldots used here and there. Cool!	commit \| commitdiff \| tree \| snapshot
2009-07-30	Claudio Sacerdoti...	First implementation of \ldots.	commit \| commitdiff \| tree \| snapshot
2009-07-30	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-30	Claudio Sacerdoti...	Don't reinvent the wheel.	commit \| commitdiff \| tree \| snapshot
2009-07-29	denes	Added benchmarks	commit \| commitdiff \| tree \| snapshot
2009-07-29	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-29	Andrea Asperti	New demodulation (innermost, optimized to avoid reducin...	commit \| commitdiff \| tree \| snapshot
2009-07-29	Andrea Asperti	Changed the ordering of rels, and the introduction...	commit \| commitdiff \| tree \| snapshot
2009-07-29	Andrea Asperti	Lazy strings	commit \| commitdiff \| tree \| snapshot
2009-07-29	Andrea Asperti	Added the benchmark with the new demodulation function.	commit \| commitdiff \| tree \| snapshot
2009-07-28	Claudio Sacerdoti...	"..." -> "\ldots" for implicit vectors	commit \| commitdiff \| tree \| snapshot
2009-07-28	Claudio Sacerdoti...	1) Some more work for vector implicits.	commit \| commitdiff \| tree \| snapshot
2009-07-28	Claudio Sacerdoti...	Introduction of vectors of implicit (only for NG).	commit \| commitdiff \| tree \| snapshot
2009-07-28	denes	New reference benchmark with CPU Time	commit \| commitdiff \| tree \| snapshot
2009-07-27	denes	Removed meaningless time information	commit \| commitdiff \| tree \| snapshot
2009-07-27	denes	Removed internal default timeout	commit \| commitdiff \| tree \| snapshot
2009-07-27	Claudio Sacerdoti...	Stupid bug fixed: the test to detect Uncertain cases...	commit \| commitdiff \| tree \| snapshot
2009-07-27	denes	Removed old logs	commit \| commitdiff \| tree \| snapshot
2009-07-27	Claudio Sacerdoti...	Useless "let module" removed.	commit \| commitdiff \| tree \| snapshot
2009-07-27	Claudio Sacerdoti...	Since I guess the divergence bug is fixed, I activate...	commit \| commitdiff \| tree \| snapshot
2009-07-27	Claudio Sacerdoti...	Serious bug fixed: because of lazy evaluation of !requi...	commit \| commitdiff \| tree \| snapshot
2009-07-27	Claudio Sacerdoti...	setoids.ma split into setoids.ma + setoids1.ma	commit \| commitdiff \| tree \| snapshot
2009-07-27	Claudio Sacerdoti...	topology/igt.ma (???) \|-> sets/setoids.ma	commit \| commitdiff \| tree \| snapshot
2009-07-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-27	denes	Moved benchmarks to new folder	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	It works better now.	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	No more hand-made coercions.	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	Record fields declared as coercions as now really decla...	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	Beta-expansion was avoided as soon as one argument...	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	Function to map NCic.term to CicNotationPt.term finished.	commit \| commitdiff \| tree \| snapshot
2009-07-24	Claudio Sacerdoti...	Bug (found during code review) fixed (but not tested...	commit \| commitdiff \| tree \| snapshot
2009-07-23	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-23	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-23	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	Elimination principles are now processed in O(1) again	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	Major speed-up: meta-chains are now expanded during...	commit \| commitdiff \| tree \| snapshot
2009-07-22	denes	Fixed test for invertibility	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	1) PTS simplified	commit \| commitdiff \| tree \| snapshot
2009-07-22	denes	Now using lazy strings for debug printings	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	nelim fixed	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	leftno was List.length rights :-)	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	Almost ready to implement coercion declaration for...	commit \| commitdiff \| tree \| snapshot
2009-07-21	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-21	Claudio Sacerdoti...	1) record projections are now automatically generated	commit \| commitdiff \| tree \| snapshot
2009-07-21	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2009-07-21	Claudio Sacerdoti...	Record projections are now automatically generated...	commit \| commitdiff \| tree \| snapshot
2009-07-21	denes	Implemented handling of Invertible equalities	commit \| commitdiff \| tree \| snapshot
2009-07-20	Enrico Tassi	sorted modules	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	Debugging printf removed	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	nrewrite now uses the appropriate principle when going...	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	nrewrite now working	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-20	denes	Removed status printing by processes	commit \| commitdiff \| tree \| snapshot
2009-07-20	denes	Fixed multiple printing	commit \| commitdiff \| tree \| snapshot
2009-07-20	Wilmer Ricciotti	Final version, submitted to CASC-22.	commit \| commitdiff \| tree \| snapshot
2009-07-20	Wilmer Ricciotti	added a flag for age selection	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	Very serious bug fixed in unification, but the fix...	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	1) The NG kernel now accepts only usage of declared...	commit \| commitdiff \| tree \| snapshot
2009-07-20	denes	One-side indexing for commutativity	commit \| commitdiff \| tree \| snapshot
2009-07-20	denes	No demod call on functionnal symbols	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	1) ppmetasenv and ppcontext to reduce the amount of...	commit \| commitdiff \| tree \| snapshot
2009-07-19	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	nelim now uses the appropriate _rect_XXX elimination...	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	1) the user is notified when a new object is defined	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	More info to refine empty types elimination.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Old code commented out.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Generation of principles is now atomic.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Debugging code commented out.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Enrico Tassi	add comment	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Non reproducible.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Some bugs already fixed.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Bugs (mostly from Oliboni)	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Bug fixed: singleton application.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	New suffixes for elimination principles:	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	1) added a function to retrieve all the universes curre...	commit \| commitdiff \| tree \| snapshot
2009-07-17	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Generation of inductive principle for Type[0].	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom