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

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

2009-09-03	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-09-03	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-09-03	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-09-02	Enrico Tassi	fix to speedup reduction making intermediate conversion...	commit \| commitdiff \| tree \| snapshot
2009-09-02	Enrico Tassi	fixed eliminator name	commit \| commitdiff \| tree \| snapshot
2009-09-02	Enrico Tassi	some work	commit \| commitdiff \| tree \| snapshot
2009-09-02	Enrico Tassi	CIC has no eta-reduction/expansion	commit \| commitdiff \| tree \| snapshot
2009-09-02	Enrico Tassi	do not fail if the inductive type is mutual, just do...	commit \| commitdiff \| tree \| snapshot
2009-09-02	Enrico Tassi	decent error on interpretation declaration	commit \| commitdiff \| tree \| snapshot
2009-09-01	Enrico Tassi	fix double app in Ast	commit \| commitdiff \| tree \| snapshot
2009-09-01	Enrico Tassi	better print of ILLEGAL applications	commit \| commitdiff \| tree \| snapshot
2009-09-01	Ferruccio Guidi	lint target improved	commit \| commitdiff \| tree \| snapshot
2009-09-01	Ferruccio Guidi	basic_rg: bugfix in AST to allow attributes in global...	commit \| commitdiff \| tree \| snapshot
2009-09-01	Enrico Tassi	catch wrapped exception	commit \| commitdiff \| tree \| snapshot
2009-08-28	Enrico Tassi	alias bug revealed	commit \| commitdiff \| tree \| snapshot
2009-08-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-08-25	Enrico Tassi	initial and incomplete port of the old demo about induc...	commit \| commitdiff \| tree \| snapshot
2009-08-25	Enrico Tassi	exponentiation should output with \sup not with ^,...	commit \| commitdiff \| tree \| snapshot
2009-08-25	Enrico Tassi	added "already defined"	commit \| commitdiff \| tree \| snapshot
2009-08-25	Enrico Tassi	ncoindutive now generates a co-inductive type, not...	commit \| commitdiff \| tree \| snapshot
2009-08-25	Enrico Tassi	Meta case not handled, the iterator was complaining.	commit \| commitdiff \| tree \| snapshot
2009-08-24	Claudio Sacerdoti...	Nicer proof "finished" (up to arithmetical facts).	commit \| commitdiff \| tree \| snapshot
2009-08-23	Ferruccio Guidi	- alpha convertibility test disabled for now (it needs...	commit \| commitdiff \| tree \| snapshot
2009-08-21	Claudio Sacerdoti...	Towards a simplified proof.	commit \| commitdiff \| tree \| snapshot
2009-08-21	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-20	Claudio Sacerdoti...	Injectivity proved! What a mess...	commit \| commitdiff \| tree \| snapshot
2009-08-20	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-20	Claudio Sacerdoti...	- Bug fixed in definition of big_op.	commit \| commitdiff \| tree \| snapshot
2009-08-20	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-20	Ferruccio Guidi	- sort inclusion must be restricted to term backbone...	commit \| commitdiff \| tree \| snapshot
2009-08-19	Claudio Sacerdoti...	One half done.	commit \| commitdiff \| tree \| snapshot
2009-08-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-17	Ferruccio Guidi	- alpha conversion check added to the brg kernel (succe...	commit \| commitdiff \| tree \| snapshot
2009-08-16	Ferruccio Guidi	- performance data added for reference	commit \| commitdiff \| tree \| snapshot
2009-08-16	Ferruccio Guidi	- proper KAM with closures implemented for the brg...	commit \| commitdiff \| tree \| snapshot
2009-08-15	Ferruccio Guidi	- kernel parameters indication added to exported object...	commit \| commitdiff \| tree \| snapshot
2009-08-14	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-14	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-14	Claudio Sacerdoti...	Since the introduction of saturation, an assert false...	commit \| commitdiff \| tree \| snapshot
2009-08-14	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-13	Ferruccio Guidi	- xml exportation activated for the brg kernel	commit \| commitdiff \| tree \| snapshot
2009-08-13	Claudio Sacerdoti...	(nat,plus) is an abelian, unital magma	commit \| commitdiff \| tree \| snapshot
2009-08-13	Claudio Sacerdoti...	Some quick patch to fix elimination that used to look for	commit \| commitdiff \| tree \| snapshot
2009-08-13	Claudio Sacerdoti...	fix_sorts (cfr. previous commit) used to break too...	commit \| commitdiff \| tree \| snapshot
2009-08-13	Claudio Sacerdoti...	Assert false do not allow to debug...	commit \| commitdiff \| tree \| snapshot
2009-08-13	Claudio Sacerdoti...	Let's refresh the universe to avoid assert failure.	commit \| commitdiff \| tree \| snapshot
2009-08-12	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-12	Claudio Sacerdoti...	A very little bit of arithmetic.	commit \| commitdiff \| tree \| snapshot
2009-08-12	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-11	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-09	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-08	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-07	Ferruccio Guidi	basic_rg: improved interface, unwind removed from appli...	commit \| commitdiff \| tree \| snapshot
2009-08-07	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-06	Claudio Sacerdoti...	The first omomorphism theorem for whole sets (i.e....	commit \| commitdiff \| tree \| snapshot
2009-08-06	Claudio Sacerdoti...	Hmmm: I don't see much gain here.	commit \| commitdiff \| tree \| snapshot
2009-08-06	Claudio Sacerdoti...	Metas must be handled when using iterators.	commit \| commitdiff \| tree \| snapshot
2009-08-06	Claudio Sacerdoti...	Setoid rewriting as unification hinting. Does not work...	commit \| commitdiff \| tree \| snapshot
2009-08-06	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-05	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-05	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-05	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-05	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-05	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-05	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-04	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-08-04	Claudio Sacerdoti...	More Gonthierism. Are they the right solution?	commit \| commitdiff \| tree \| snapshot
2009-08-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-08-04	Claudio Sacerdoti...	Hmmm, quite broken now.	commit \| commitdiff \| tree \| snapshot
2009-08-04	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom