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

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

2007-09-13	Claudio Sacerdoti...	added a debug print	commit \| commitdiff \| tree \| snapshot
2007-09-12	Ferruccio Guidi	rdfly patched to work with the new db structure	commit \| commitdiff \| tree \| snapshot
2007-09-12	Wilmer Ricciotti	Updated, proofs are now about 750 lines.	commit \| commitdiff \| tree \| snapshot
2007-09-11	Ferruccio Guidi	librarySync - we do not generate the object attributes...	commit \| commitdiff \| tree \| snapshot
2007-09-11	Cristian Armentano	some theorem names changed.	commit \| commitdiff \| tree \| snapshot
2007-09-11	Enrico Tassi	replaced an assert false that cause nat_ind not to...	commit \| commitdiff \| tree \| snapshot
2007-09-10	Enrico Tassi	last version with caml 3.09 built and saved as 0.3.0	commit \| commitdiff \| tree \| snapshot
2007-09-10	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2007-09-10	Cristian Armentano	other simplifications.	commit \| commitdiff \| tree \| snapshot
2007-09-10	Claudio Sacerdoti...	This test shows one of the few cases were Matita is...	commit \| commitdiff \| tree \| snapshot
2007-09-09	Stefano Zacchiroli	* debian/control	commit \| commitdiff \| tree \| snapshot
2007-09-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2007-09-09	Enrico Tassi	in the case of coerce_to_sort the whd was done with...	commit \| commitdiff \| tree \| snapshot
2007-09-09	Cristian Armentano	other simplifications.	commit \| commitdiff \| tree \| snapshot
2007-09-09	Stefano Zacchiroli	* NOT RELEASED YET	commit \| commitdiff \| tree \| snapshot
2007-09-09	Stefano Zacchiroli	* change how the ocamldoc API reference is generated...	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	huge commit regarding coercions to funclass and eat_pro...	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	the order of abstraction is now correct, but there...	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	removed an assertion that makes no more sense to me	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	better debug printings	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	better test for church numerals	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	just a Pcre expression fixed, nothing real	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	matita can now safely start a matitac that will put...	commit \| commitdiff \| tree \| snapshot
2007-09-08	Enrico Tassi	Full specification of find. Added notation for If_Then_...	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	bump version	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	release	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	* add ocamldoc comments to .mli interface files	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	include also gdome2/ dir in the ocamldoc include path	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	* debian/rules	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	why the heck configure was committed?	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	* debian/control	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	init new dummy entry	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	remove spurious comment	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	upload to unstable	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	remove spurious entry	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	- s/Source-Version/binary:Version/ substvar	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	add stdlib/gdome2 to the include dir for ocamldoc	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	bump version	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	* convert comments in .mli interface files to ocamldoc...	commit \| commitdiff \| tree \| snapshot
2007-09-08	Stefano Zacchiroli	convert comments to ocamldoc comments	commit \| commitdiff \| tree \| snapshot
2007-09-07	Enrico Tassi	1. fix_arity fixed: the code is totally wrong and this...	commit \| commitdiff \| tree \| snapshot
2007-09-07	Enrico Tassi	This cast now works!	commit \| commitdiff \| tree \| snapshot
2007-09-07	Enrico Tassi	when a coercion is passed through a case on right-param...	commit \| commitdiff \| tree \| snapshot
2007-09-07	Cristian Armentano	some simplifications.	commit \| commitdiff \| tree \| snapshot
2007-09-07	Enrico Tassi	ooops, missing )	commit \| commitdiff \| tree \| snapshot
2007-09-07	Enrico Tassi	disabled coercions when refining paramod proofs (attemt...	commit \| commitdiff \| tree \| snapshot
2007-09-07	Enrico Tassi	fixed propagation under Fix/Lambda/Case of coercions...	commit \| commitdiff \| tree \| snapshot
2007-09-06	Cristian Armentano	Some simplifications.	commit \| commitdiff \| tree \| snapshot
2007-09-06	Enrico Tassi	coercions under Fix and Case. Code refactoring needed	commit \| commitdiff \| tree \| snapshot
2007-09-06	Enrico Tassi	added a duplicated implementation of replace lifting	commit \| commitdiff \| tree \| snapshot
2007-09-06	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2007-09-05	Ferruccio Guidi	- lybrarySync:	commit \| commitdiff \| tree \| snapshot
2007-09-05	Ferruccio Guidi	- matitaInit matitaprover matitadep matitamake:	commit \| commitdiff \| tree \| snapshot
2007-09-05	Claudio Sacerdoti...	added fix case	commit \| commitdiff \| tree \| snapshot
2007-09-05	Claudio Sacerdoti...	coercions are propagated under Fix (but not mutually...	commit \| commitdiff \| tree \| snapshot
2007-09-04	Claudio Sacerdoti...	Dandling ")" removed from notation for 'exists.	commit \| commitdiff \| tree \| snapshot
2007-09-04	Claudio Sacerdoti...	Composition of coercions with arity > 0 is now implemen...	commit \| commitdiff \| tree \| snapshot
2007-09-04	Claudio Sacerdoti...	A test for propagation of coercions (that open new...	commit \| commitdiff \| tree \| snapshot
2007-09-04	Claudio Sacerdoti...	1. composition of coercions with saturations > 0 is...	commit \| commitdiff \| tree \| snapshot
2007-08-31	Claudio Sacerdoti...	alpha conversion to avoid case-insensitivity of MySql...	commit \| commitdiff \| tree \| snapshot
2007-08-31	Claudio Sacerdoti...	baseuri changed	commit \| commitdiff \| tree \| snapshot
2007-08-31	Enrico Tassi	fixed coercions between arrows when the arrow is dependent.	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	captured exception preserved (was replaced blindly...	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	reverted assertion, since it may happen to look for...	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	refactoring of all coercions code and add a check to...	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	bugfix in computation of src and tgt for coercions...	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	tests for coercions under lambdas	commit \| commitdiff \| tree \| snapshot
2007-08-30	Claudio Sacerdoti...	Coercions are now generalized to the general form	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	Coercions rework:	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	coercions from funclass are not supported	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	bla bla bla fallback	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	added a binch of svn:ignore	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	add a fallback in case the binaries are in the path...	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	print few more wired assertions	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	the version on the livecd	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	more stuff to reach an intensional definition of finite...	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	added an utility function	commit \| commitdiff \| tree \| snapshot
2007-08-30	Enrico Tassi	0.2.0	commit \| commitdiff \| tree \| snapshot
2007-08-28	Claudio Sacerdoti...	* definition of implication free propositional formulas	commit \| commitdiff \| tree \| snapshot
2007-08-28	Claudio Sacerdoti...	A primer for Matita with some easy, medium, difficult...	commit \| commitdiff \| tree \| snapshot
2007-08-26	Ferruccio Guidi	We define proof tree tracks and normal proof tree track...	commit \| commitdiff \| tree \| snapshot
2007-08-26	Ferruccio Guidi	refactoring	commit \| commitdiff \| tree \| snapshot
2007-08-26	Ferruccio Guidi	proof by "introduction" (impi) implemented in full	commit \| commitdiff \| tree \| snapshot
2007-08-25	Claudio Sacerdoti...	thread-based interface activated again	commit \| commitdiff \| tree \| snapshot
2007-08-23	Claudio Sacerdoti...	Bug fixed: RewriteLR were not recognized correctly...	commit \| commitdiff \| tree \| snapshot
2007-08-23	Claudio Sacerdoti...	Bug fixed: the initial metasenv used in the two tactic...	commit \| commitdiff \| tree \| snapshot
2007-08-22	Claudio Sacerdoti...	Avoid reusing Hbeta several times.	commit \| commitdiff \| tree \| snapshot
2007-08-22	Claudio Sacerdoti...	select now works correctly even if multiple hypotheses...	commit \| commitdiff \| tree \| snapshot
2007-08-21	Claudio Sacerdoti...	Avoid confusion for names of proofs put in the applicat...	commit \| commitdiff \| tree \| snapshot
2007-08-21	Claudio Sacerdoti...	"obtain H E1=E2 by proof" is now working	commit \| commitdiff \| tree \| snapshot
2007-08-16	Cristian Armentano	little change to theorem eq_gcd_times_times_eqv_times_gcd	commit \| commitdiff \| tree \| snapshot
2007-07-31	Andrea Asperti	removed generic_sigma_p since generic_iter_p is the...	commit \| commitdiff \| tree \| snapshot
2007-07-31	Enrico Tassi	something was really too slow...	commit \| commitdiff \| tree \| snapshot
2007-07-31	Enrico Tassi	default equality stuff filtered out from hint rewrite	commit \| commitdiff \| tree \| snapshot
2007-07-31	Enrico Tassi	removed comments in proof presentation	commit \| commitdiff \| tree \| snapshot
2007-07-30	Cristian Armentano	renamed generic_sigma_p.ma to generic_iter_p.ma	commit \| commitdiff \| tree \| snapshot
2007-07-30	Enrico Tassi	added 'rewrite' option to the the hint macro. a cicBrow...	commit \| commitdiff \| tree \| snapshot
2007-07-26	Ferruccio Guidi	We add a binary for computing the "heights" of helm...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom