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

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

2009-09-17	Enrico Tassi	more work for igft	commit \| commitdiff \| tree \| snapshot
2009-09-16	Enrico Tassi	more notation for topologies, and some prentheses that...	commit \| commitdiff \| tree \| snapshot
2009-09-16	Enrico Tassi	some more work...	commit \| commitdiff \| tree \| snapshot
2009-09-16	Claudio Sacerdoti...	New interesting coercion.	commit \| commitdiff \| tree \| snapshot
2009-09-16	Claudio Sacerdoti...	The left parameters coming from the constructor types...	commit \| commitdiff \| tree \| snapshot
2009-09-15	Enrico Tassi	improved check in delift for flexible lc entries.	commit \| commitdiff \| tree \| snapshot
2009-09-15	Ferruccio Guidi	some renaming. final commit for version 0.8.0	commit \| commitdiff \| tree \| snapshot
2009-09-14	Enrico Tassi	fixed coercion mechanism w.r.t. undo/require	commit \| commitdiff \| tree \| snapshot
2009-09-14	Claudio Sacerdoti...	Slightly simplied status code.	commit \| commitdiff \| tree \| snapshot
2009-09-14	Claudio Sacerdoti...	Simplest typing for status records.	commit \| commitdiff \| tree \| snapshot
2009-09-14	Claudio Sacerdoti...	New tactics ncut and nlapply.	commit \| commitdiff \| tree \| snapshot
2009-09-13	Enrico Tassi	a nice bug in meta handling is not visible... brr...	commit \| commitdiff \| tree \| snapshot
2009-09-13	Enrico Tassi	some more letters	commit \| commitdiff \| tree \| snapshot
2009-09-11	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-11	Enrico Tassi	constructor accepts the arguments of the constructor...	commit \| commitdiff \| tree \| snapshot
2009-09-11	Enrico Tassi	new tactic constructor: @[n]	commit \| commitdiff \| tree \| snapshot
2009-09-11	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-11	Enrico Tassi	new syntax	commit \| commitdiff \| tree \| snapshot
2009-09-11	Enrico Tassi	let rec/corec and co/inductive are not printed!	commit \| commitdiff \| tree \| snapshot
2009-09-11	Enrico Tassi	new macro ncheck. fixed term2pres for Inductive and...	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	ok, but slow on includes	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	nice hints	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	maledetto il \sub di CSC	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	it starts to work	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	nice notation for hints!	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	allow @{ ... } as the identifier of the letin	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	to me, the problem:	commit \| commitdiff \| tree \| snapshot
2009-09-10	Ferruccio Guidi	some interfaces improved	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	more stuff fixed	commit \| commitdiff \| tree \| snapshot
2009-09-10	Enrico Tassi	the refiner was not checking that the resulting type	commit \| commitdiff \| tree \| snapshot
2009-09-09	Enrico Tassi	some fixes here and there	commit \| commitdiff \| tree \| snapshot
2009-09-09	Enrico Tassi	depends	commit \| commitdiff \| tree \| snapshot
2009-09-09	Enrico Tassi	some more work for ng-coercions	commit \| commitdiff \| tree \| snapshot
2009-09-08	Ferruccio Guidi	some renaming and some interfaces improved	commit \| commitdiff \| tree \| snapshot
2009-09-08	Enrico Tassi	snapshot for CSC	commit \| commitdiff \| tree \| snapshot
2009-09-08	Enrico Tassi	snapshot for CSC	commit \| commitdiff \| tree \| snapshot
2009-09-05	Ferruccio Guidi	basic_rg: more improvements to the error reporting...	commit \| commitdiff \| tree \| snapshot
2009-09-05	Ferruccio Guidi	basic_rg: we improved the error reporting interface	commit \| commitdiff \| tree \| snapshot
2009-09-04	Ferruccio Guidi	the TypeError exception is back in place inside the...	commit \| commitdiff \| tree \| snapshot
2009-09-04	Enrico Tassi	Reduction speedup (a.k.a. better sharing):	commit \| commitdiff \| tree \| snapshot
2009-09-04	Enrico Tassi	Reduction speedup (a.k.a. better sharing):	commit \| commitdiff \| tree \| snapshot
2009-09-04	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-09-04	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-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
next

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

RSS Atom