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

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

2006-12-07	Stefano Zacchiroli	reverted error committed by mistake	commit \| commitdiff \| tree \| snapshot
2006-12-07	Stefano Zacchiroli	avoid Failure "nth" when only one disambiguation pass...	commit \| commitdiff \| tree \| snapshot
2006-12-07	Ferruccio Guidi	new theorems added. does not comile well yet :(( proble...	commit \| commitdiff \| tree \| snapshot
2006-12-06	Claudio Sacerdoti...	Experimental: cycles in proofs generated by paramodulat...	commit \| commitdiff \| tree \| snapshot
2006-12-06	Claudio Sacerdoti...	More simplification using better notation.	commit \| commitdiff \| tree \| snapshot
2006-12-06	Claudio Sacerdoti...	interactive and bad_tests grepped out before insertion...	commit \| commitdiff \| tree \| snapshot
2006-12-05	Stefano Zacchiroli	experimental classification of disambiguation error...	commit \| commitdiff \| tree \| snapshot
2006-12-05	Ferruccio Guidi	- components: composed coercions mus be generated with...	commit \| commitdiff \| tree \| snapshot
2006-12-05	Stefano Zacchiroli	do not share the db connection among children, should...	commit \| commitdiff \| tree \| snapshot
2006-12-01	Ferruccio Guidi	prova.ma: baseuri fixed	commit \| commitdiff \| tree \| snapshot
2006-12-01	Ferruccio Guidi	some uris fixed	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	Even if automatically generated, I prefer to commit...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	Notation \middot used everywhere in place of *.	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	I have changed the nice notation for derivatives a...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	Added a demo for Matita: two slightly different proofs...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	Syntax of a declarative rewritinstep changed.	commit \| commitdiff \| tree \| snapshot
2006-11-30	Wilmer Ricciotti	library/Fsub: minor fix	commit \| commitdiff \| tree \| snapshot
2006-11-30	Wilmer Ricciotti	library: added solution to POPLMark challenge part...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	New syntax and semantics for the rewriting steps that...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	The auto parameters that can be given to a declarative...	commit \| commitdiff \| tree \| snapshot
2006-11-29	Claudio Sacerdoti...	The rewritingstep declarative command now takes also...	commit \| commitdiff \| tree \| snapshot
2006-11-29	Ferruccio Guidi	- new library/logic/coimplication.ma uses new decompose...	commit \| commitdiff \| tree \| snapshot
2006-11-29	Ferruccio Guidi	- decompose tactic: decomposable constants are now...	commit \| commitdiff \| tree \| snapshot
2006-11-29	Andrea Asperti	Demodulate_tac now depends on the universe	commit \| commitdiff \| tree \| snapshot
2006-11-28	Claudio Sacerdoti...	Added a clear to rewritestep to speed up auto (by remov...	commit \| commitdiff \| tree \| snapshot
2006-11-28	Andrea Asperti	Changed an ahstable into an association list.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Claudio Sacerdoti...	"the thesis becomes" now always performs a change.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Claudio Sacerdoti...	Fixed bug in notation: when a notation is applied to...	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Added in_eq_uris.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Fix_proof should recursively work on explicit substs.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Claudio Sacerdoti...	Declarative language ported to new auto (with Universes).	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Removed a couple of assertions.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Commented an assertion.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Commented an assertion.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Commented a few assertions.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Variant are not indexed.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Only modified for taking unfold into account.	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Matita's default equality has changed	commit \| commitdiff \| tree \| snapshot
2006-11-27	Andrea Asperti	Small changes	commit \| commitdiff \| tree \| snapshot
2006-11-27	Claudio Sacerdoti...	auto new => auto new library in those tests that use...	commit \| commitdiff \| tree \| snapshot
2006-11-25	Enrico Tassi	fix	commit \| commitdiff \| tree \| snapshot
2006-11-25	Enrico Tassi	patch to calculate meets of a pair of carriers	commit \| commitdiff \| tree \| snapshot
2006-11-25	Enrico Tassi	added assertion (that is a TODO) in case non-considered...	commit \| commitdiff \| tree \| snapshot
2006-11-25	Enrico Tassi	added a test for the pullback stuff and the possibility...	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Command index added to disambiguate.	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Added a new command "index" for the indexing terms...	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Set of Set of uri added.	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Modifications to auto due to the introduction of the...	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Universe is a discrimination-tree structure.	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	The status has been extended with a "universe", that...	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Fixed a call to auto, and commented the remaining part.	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	paramodulation removed	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Minor changes.	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Simplified version.	commit \| commitdiff \| tree \| snapshot
2006-11-23	Andrea Asperti	Adding CoRN.	commit \| commitdiff \| tree \| snapshot
2006-11-22	Ferruccio Guidi	removed the impredicativity of falsum	commit \| commitdiff \| tree \| snapshot
2006-11-17	Claudio Sacerdoti...	Fixed the infamous bug:	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom