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

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

2009-09-27	Enrico Tassi	Type printed as such, CProp printed as such	commit \| commitdiff \| tree \| snapshot
2009-09-27	Enrico Tassi	fixpoint have attributes for pragma (i.e. they can...	commit \| commitdiff \| tree \| snapshot
2009-09-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-25	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-24	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-24	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-24	Enrico Tassi	multi screenshot	commit \| commitdiff \| tree \| snapshot
2009-09-24	Enrico Tassi	ncheck works in the current ctx	commit \| commitdiff \| tree \| snapshot
2009-09-24	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-24	Enrico Tassi	....	commit \| commitdiff \| tree \| snapshot
2009-09-23	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-23	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-23	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-23	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-23	Enrico Tassi	more on screenshot	commit \| commitdiff \| tree \| snapshot
2009-09-23	Enrico Tassi	new macro screenshot	commit \| commitdiff \| tree \| snapshot
2009-09-22	Ferruccio Guidi	we improved the stylesheets and we generated the static...	commit \| commitdiff \| tree \| snapshot
2009-09-22	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-21	Ferruccio Guidi	xml: bug fix	commit \| commitdiff \| tree \| snapshot
2009-09-21	Ferruccio Guidi	xml: first ld to xml stylesheets	commit \| commitdiff \| tree \| snapshot
2009-09-21	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-09-21	Enrico Tassi	new tactics by CSC	commit \| commitdiff \| tree \| snapshot
2009-09-21	Enrico Tassi	new implementation of delift_type_wrt_term, that call...	commit \| commitdiff \| tree \| snapshot
2009-09-21	Enrico Tassi	huge commit regarding universes:	commit \| commitdiff \| tree \| snapshot
2009-09-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-09-17	Ferruccio Guidi	we start version 0.8.1 by replacing the abstract layer...	commit \| commitdiff \| tree \| snapshot
2009-09-17	Enrico Tassi	one more exception printed	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom