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

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

2006-11-17	Ferruccio Guidi	helm_registry: added the pair unmarshaller	commit \| commitdiff \| tree \| snapshot
2006-11-17	Ferruccio Guidi	CoRN-Decl: missing file added	commit \| commitdiff \| tree \| snapshot
2006-11-16	Ferruccio Guidi	- transcript: patched to generate CoRN_notation.ma...	commit \| commitdiff \| tree \| snapshot
2006-11-16	Ferruccio Guidi	- transcript: now outputs includes and coercions correctly	commit \| commitdiff \| tree \| snapshot
2006-11-15	Ferruccio Guidi	new CoRN development, generated by transcript	commit \| commitdiff \| tree \| snapshot
2006-11-15	Ferruccio Guidi	transcript updated	commit \| commitdiff \| tree \| snapshot
2006-11-15	Ferruccio Guidi	removed prived CoRN configuration file :)	commit \| commitdiff \| tree \| snapshot
2006-11-15	Ferruccio Guidi	transcript: very alpha version.	commit \| commitdiff \| tree \| snapshot
2006-11-15	Ferruccio Guidi	fixed base uri	commit \| commitdiff \| tree \| snapshot
2006-11-15	Andrea Asperti	lt_O_S moved to nat/orders.ma	commit \| commitdiff \| tree \| snapshot
2006-11-15	Andrea Asperti	Added lt_O_S.	commit \| commitdiff \| tree \| snapshot
2006-11-14	Claudio Sacerdoti...	&TODO => &TODO;	commit \| commitdiff \| tree \| snapshot
2006-11-14	maiorino	New: on-line help for declarative tactics (first version).	commit \| commitdiff \| tree \| snapshot
2006-11-14	Claudio Sacerdoti...	library=1 in obtain _ = _ by _.	commit \| commitdiff \| tree \| snapshot
2006-11-12	Claudio Sacerdoti...	The pretty printers in CicPp now have an optional ...	commit \| commitdiff \| tree \| snapshot
2006-11-11	Ferruccio Guidi	NLE is now derived fron NPlus rather than being a stand...	commit \| commitdiff \| tree \| snapshot
2006-11-10	Enrico Zoli	Dama: up to L-spaces and the proof (completed up to...	commit \| commitdiff \| tree \| snapshot
2006-11-06	Enrico Zoli	More work on groups, real numbers and integration algebras.	commit \| commitdiff \| tree \| snapshot
2006-11-05	Claudio Sacerdoti...	Some clean-up here and there in dama (coercions removed...	commit \| commitdiff \| tree \| snapshot
2006-11-05	Claudio Sacerdoti...	Almost every hand-inserted coercion removed since a...	commit \| commitdiff \| tree \| snapshot
2006-11-05	Claudio Sacerdoti...	Bug fixed: the disambiguation domain for a record with...	commit \| commitdiff \| tree \| snapshot
2006-11-05	Claudio Sacerdoti...	Critical bug finally found after a long chasing!!!	commit \| commitdiff \| tree \| snapshot
2006-11-05	Claudio Sacerdoti...	Added more typing information to remove a coercion.	commit \| commitdiff \| tree \| snapshot
2006-11-03	Enrico Zoli	Integration f_algebras declassed.	commit \| commitdiff \| tree \| snapshot
2006-11-03	Enrico Zoli	Up to absolute value	commit \| commitdiff \| tree \| snapshot
2006-11-03	Stefano Zacchiroli	preliminary support for hbugs	commit \| commitdiff \| tree \| snapshot
2006-11-03	Enrico Zoli	Up to max (up to a bug).	commit \| commitdiff \| tree \| snapshot
2006-10-31	Enrico Zoli	We begin to play the real game: we have defined real...	commit \| commitdiff \| tree \| snapshot
2006-10-31	Enrico Zoli	Integration_algebras.ma split into 6 different files.	commit \| commitdiff \| tree \| snapshot
2006-10-31	Enrico Zoli	Syntax changed (to be changed back) for left parameters...	commit \| commitdiff \| tree \| snapshot
2006-10-31	Claudio Sacerdoti...	The OK button of the disambiguation errors interface...	commit \| commitdiff \| tree \| snapshot
2006-10-31	Claudio Sacerdoti...	Bug fixed: inductive types were no longer removed from...	commit \| commitdiff \| tree \| snapshot
2006-10-31	Claudio Sacerdoti...	New behaviour of the disambiguation error messages...	commit \| commitdiff \| tree \| snapshot
2006-10-30	Claudio Sacerdoti...	TermAcicContent.Interpretation_not_found catched and...	commit \| commitdiff \| tree \| snapshot
2006-10-30	Claudio Sacerdoti...	Up to integration f-algebras.	commit \| commitdiff \| tree \| snapshot
2006-10-30	Claudio Sacerdoti...	Debugging code is now controlled by the debug flag.	commit \| commitdiff \| tree \| snapshot
2006-10-30	Andrea Asperti	library = yes!	commit \| commitdiff \| tree \| snapshot
2006-10-30	Claudio Sacerdoti...	remove_obj is now much faster:	commit \| commitdiff \| tree \| snapshot
2006-10-29	Ferruccio Guidi	Level-1/LambdaDelta now compiles fine	commit \| commitdiff \| tree \| snapshot
2006-10-29	Claudio Sacerdoti...	Added target preall.opt.	commit \| commitdiff \| tree \| snapshot
2006-10-28	Claudio Sacerdoti...	GRAVE BUG IN COERCIONS FIXED: the insertion of a coerci...	commit \| commitdiff \| tree \| snapshot
2006-10-26	Claudio Sacerdoti...	Better label for the disambiguation errors window.	commit \| commitdiff \| tree \| snapshot
2006-10-26	Claudio Sacerdoti...	New (and much more complex) disambiguation error interface.	commit \| commitdiff \| tree \| snapshot
2006-10-26	Claudio Sacerdoti...	More timeout added to autos here and there.	commit \| commitdiff \| tree \| snapshot
2006-10-25	Claudio Sacerdoti...	1. is_meta_closed should be applied only to terms on...	commit \| commitdiff \| tree \| snapshot
2006-10-25	Ferruccio Guidi	till some patches	commit \| commitdiff \| tree \| snapshot
2006-10-25	Ferruccio Guidi	the incomplete proofs were axiomatized	commit \| commitdiff \| tree \| snapshot
2006-10-25	Ferruccio Guidi	some patches. still does not compile properly	commit \| commitdiff \| tree \| snapshot
2006-10-25	Claudio Sacerdoti...	Added timeouts to auto here and there.	commit \| commitdiff \| tree \| snapshot
2006-10-25	Claudio Sacerdoti...	Added timeout to autos here and there.	commit \| commitdiff \| tree \| snapshot
2006-10-25	Claudio Sacerdoti...	1. bug fixed: Unicode characters that are not mapped...	commit \| commitdiff \| tree \| snapshot
2006-10-25	Claudio Sacerdoti...	/home/fguidi/... => ../../...	commit \| commitdiff \| tree \| snapshot
2006-10-25	Ferruccio Guidi	we removed about 100 match-with costruction turning...	commit \| commitdiff \| tree \| snapshot
2006-10-25	Andrea Asperti	Added a couple of flags to auto	commit \| commitdiff \| tree \| snapshot
2006-10-25	Claudio Sacerdoti...	Our unification used to guess a very complex argument...	commit \| commitdiff \| tree \| snapshot
2006-10-25	Claudio Sacerdoti...	Two lemmas that used to pass no more now pass again...	commit \| commitdiff \| tree \| snapshot
2006-10-24	Enrico Zoli	Added unit to rings.	commit \| commitdiff \| tree \| snapshot
2006-10-24	Enrico Zoli	More coercions added in the algebraic hierarchy.	commit \| commitdiff \| tree \| snapshot
2006-10-24	Enrico Zoli	Up to f_algebras.	commit \| commitdiff \| tree \| snapshot
2006-10-24	Enrico Tassi	fixed the ugly button added by csc, now it is inside...	commit \| commitdiff \| tree \| snapshot
2006-10-24	Enrico Tassi	removed equality_retrieval	commit \| commitdiff \| tree \| snapshot
2006-10-23	Claudio Sacerdoti...	Better (and more localized) error message for sort_of_prod.	commit \| commitdiff \| tree \| snapshot
2006-10-23	Claudio Sacerdoti...	CicUniv.UniverseInconsistency is no handled correcly.	commit \| commitdiff \| tree \| snapshot
2006-10-23	Claudio Sacerdoti...	binaries/saturate no longer compiled since it does...	commit \| commitdiff \| tree \| snapshot
2006-10-20	Andrea Asperti	Demodulate and applyS moved form saturation to auto.	commit \| commitdiff \| tree \| snapshot
2006-10-20	Andrea Asperti	Major changes to auto, documented on the helm mailing...	commit \| commitdiff \| tree \| snapshot
2006-10-20	Andrea Asperti	Minor changes.	commit \| commitdiff \| tree \| snapshot
2006-10-20	Andrea Asperti	a. uniform mangement for context and library	commit \| commitdiff \| tree \| snapshot
2006-10-20	Andrea Asperti	The type of universe_of_goals has slightly changed...	commit \| commitdiff \| tree \| snapshot
2006-10-20	Andrea Asperti	This is only a temporary patch. The typecheker raises a	commit \| commitdiff \| tree \| snapshot
2006-10-20	Andrea Asperti	The function exists_a_meta has been modified to capture...	commit \| commitdiff \| tree \| snapshot
2006-10-20	Andrea Asperti	New function pack_coercion_metasenv, used in auto after...	commit \| commitdiff \| tree \| snapshot
2006-10-20	Enrico Zoli	Up to f_algebras.	commit \| commitdiff \| tree \| snapshot
2006-10-20	Enrico Zoli	1. developed up to algebras	commit \| commitdiff \| tree \| snapshot
2006-10-20	Enrico Zoli	Serious bug fixed: without a Lazy.force the user obtain...	commit \| commitdiff \| tree \| snapshot
2006-10-19	Claudio Sacerdoti...	Disambiguation errors are now compressed in a maybe...	commit \| commitdiff \| tree \| snapshot
2006-10-19	Claudio Sacerdoti...	Bug fixed: when trying to insert coercions after an...	commit \| commitdiff \| tree \| snapshot
2006-10-19	Claudio Sacerdoti...	Potential performance improvement + better disambiguati...	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	Missing optimization implemented: before starting to...	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	- Disambiguation error exception enriched with more...	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	Bug fixed: the diff component of the exception raised...	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	EXPERIMENTAL: new interface for disambiguation errors.	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	Dead dialog window removed.	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	Dead dialog window removed.	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	Disambiguation errors now carry more information (i...	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	Dama is now in the night benchmarks.	commit \| commitdiff \| tree \| snapshot
2006-10-18	Claudio Sacerdoti...	Too verbose error message (probably activated by Enrico...	commit \| commitdiff \| tree \| snapshot
2006-10-17	Ferruccio Guidi	new objects for the LambdaDelta development (4th conjec...	commit \| commitdiff \| tree \| snapshot
2006-10-17	Ferruccio Guidi	more new objects for the LambdaDelta contribution	commit \| commitdiff \| tree \| snapshot
2006-10-16	Enrico Zoli	Beginning of the development of integration algebras.	commit \| commitdiff \| tree \| snapshot
2006-10-13	Claudio Sacerdoti...	Content level representation of LetRec changed.	commit \| commitdiff \| tree \| snapshot
2006-10-13	Claudio Sacerdoti...	Content level representation of LetRec changed.	commit \| commitdiff \| tree \| snapshot
2006-10-13	Claudio Sacerdoti...	New content level representations for LetRec, Inductive...	commit \| commitdiff \| tree \| snapshot
2006-10-12	Ferruccio Guidi	files with newest objects (to be included in the respec...	commit \| commitdiff \| tree \| snapshot
2006-10-12	Enrico Tassi	carr_of_term now returns Fun if a Prod is encountered	commit \| commitdiff \| tree \| snapshot
2006-10-12	Enrico Tassi	fixed defaultauto behaviour. not the cache is preserveed	commit \| commitdiff \| tree \| snapshot
2006-10-12	Enrico Tassi	timeout if unspecfied should be set to infinity, not...	commit \| commitdiff \| tree \| snapshot
2006-10-12	Claudio Sacerdoti...	The default for paramodulation is now back to false...	commit \| commitdiff \| tree \| snapshot
2006-10-12	acciavat	auto => auto new.	commit \| commitdiff \| tree \| snapshot
2006-10-12	Claudio Sacerdoti...	Inclusion "improved".	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom