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

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

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
2007-07-26	Enrico Tassi	added development path normalization, inclusions with...	commit \| commitdiff \| tree \| snapshot
2007-07-26	Enrico Tassi	auto -> autobatch	commit \| commitdiff \| tree \| snapshot
2007-07-26	Wilmer Ricciotti	Some notation added	commit \| commitdiff \| tree \| snapshot
2007-07-26	Enrico Tassi	more stuff about coercions	commit \| commitdiff \| tree \| snapshot
2007-07-26	Enrico Tassi	little bug in coercion generation found. it use to...	commit \| commitdiff \| tree \| snapshot
2007-07-26	Ferruccio Guidi	makefiles updated	commit \| commitdiff \| tree \| snapshot
2007-07-25	Ferruccio Guidi	makefile updated	commit \| commitdiff \| tree \| snapshot
2007-07-25	Ferruccio Guidi	matitac: We do not generate the .moo and .lexicon of...	commit \| commitdiff \| tree \| snapshot
2007-07-25	Enrico Tassi	added some notation	commit \| commitdiff \| tree \| snapshot
2007-07-25	Enrico Tassi	added another example in which our coercions are powerful	commit \| commitdiff \| tree \| snapshot
2007-07-25	Enrico Tassi	used ;try assumption instead of .try assumption	commit \| commitdiff \| tree \| snapshot
2007-07-25	Enrico Tassi	; and not . after auto-paramodulation	commit \| commitdiff \| tree \| snapshot
2007-07-25	Enrico Tassi	reverted previous fix	commit \| commitdiff \| tree \| snapshot
2007-07-25	Enrico Tassi	restored compaction of metas at the end of given_clause	commit \| commitdiff \| tree \| snapshot
2007-07-24	Ferruccio Guidi	Makefile missing in previous commit	commit \| commitdiff \| tree \| snapshot
2007-07-24	Ferruccio Guidi	New developement LOGIC about the cut elimination of...	commit \| commitdiff \| tree \| snapshot
2007-07-24	Enrico Tassi	added test about dependent coercions	commit \| commitdiff \| tree \| snapshot
2007-07-23	Claudio Sacerdoti...	Prototype of min_aux changed.	commit \| commitdiff \| tree \| snapshot
2007-07-23	Ferruccio Guidi	auto vs autobatch fixed	commit \| commitdiff \| tree \| snapshot
2007-07-23	Ferruccio Guidi	autobatch parameters reajusted	commit \| commitdiff \| tree \| snapshot
2007-07-23	Enrico Tassi	fixed makefiles to make it compile cleanly again	commit \| commitdiff \| tree \| snapshot
2007-07-22	Ferruccio Guidi	Procedural: the statement body and it inner types must...	commit \| commitdiff \| tree \| snapshot
2007-07-20	Claudio Sacerdoti...	Another nicer version.	commit \| commitdiff \| tree \| snapshot
2007-07-20	Claudio Sacerdoti...	Even nicer script.	commit \| commitdiff \| tree \| snapshot
2007-07-20	Claudio Sacerdoti...	The nicest script obtained so far.	commit \| commitdiff \| tree \| snapshot
2007-07-20	Ferruccio Guidi	acic_procedural: bug fix:	commit \| commitdiff \| tree \| snapshot
2007-07-20	Claudio Sacerdoti...	More simplification due to the new conversion strategy.	commit \| commitdiff \| tree \| snapshot
2007-07-20	Claudio Sacerdoti...	Script simplification due to the new efficient conversi...	commit \| commitdiff \| tree \| snapshot
2007-07-20	Claudio Sacerdoti...	Tentative bug fix for diverging pretty-printing function.	commit \| commitdiff \| tree \| snapshot
2007-07-20	Claudio Sacerdoti...	Initialization of matita.map_unicode_to_tex moved from...	commit \| commitdiff \| tree \| snapshot
2007-07-19	Ferruccio Guidi	cicUtil : new test function "is_sober" to test...	commit \| commitdiff \| tree \| snapshot
2007-07-19	Claudio Sacerdoti...	Convertibility now converts machines in place of terms.	commit \| commitdiff \| tree \| snapshot
2007-07-19	Claudio Sacerdoti...	map_unicode_to_tex is no longer optional and it always...	commit \| commitdiff \| tree \| snapshot
2007-07-19	Claudio Sacerdoti...	paste_unicode_as_tex is now false by default; moreover...	commit \| commitdiff \| tree \| snapshot
2007-07-19	Enrico Tassi	COERCIONS: tentative addition of an equivalence relatio...	commit \| commitdiff \| tree \| snapshot
2007-07-19	Enrico Tassi	the cade was escaping the table name and not the uri	commit \| commitdiff \| tree \| snapshot
2007-07-19	Enrico Tassi	fixed escaping for sqlite	commit \| commitdiff \| tree \| snapshot
2007-07-19	Enrico Tassi	fixed an escaping error, added more infos to the generi...	commit \| commitdiff \| tree \| snapshot
2007-07-19	Claudio Sacerdoti...	Typo fixed.	commit \| commitdiff \| tree \| snapshot
2007-07-19	Claudio Sacerdoti...	Super-nice notation for the assembly stuff.	commit \| commitdiff \| tree \| snapshot
2007-07-18	Ferruccio Guidi	the predicate for elim was not built correctly when...	commit \| commitdiff \| tree \| snapshot
2007-07-18	Enrico Tassi	recursive argument in let rec is not printed explicitly.	commit \| commitdiff \| tree \| snapshot
2007-07-18	Enrico Tassi	fixed coercion graph print, moved coercion graph and...	commit \| commitdiff \| tree \| snapshot
2007-07-17	Claudio Sacerdoti...	added missing parenthesis	commit \| commitdiff \| tree \| snapshot
2007-07-17	Enrico Tassi	fixed includes and added notation for bytes	commit \| commitdiff \| tree \| snapshot
2007-07-16	Claudio Sacerdoti...	More lemmas.	commit \| commitdiff \| tree \| snapshot
2007-07-16	Claudio Sacerdoti...	More daemons closed. A couple left in byte and many...	commit \| commitdiff \| tree \| snapshot
2007-07-16	Claudio Sacerdoti...	More daemons/axioms closed.	commit \| commitdiff \| tree \| snapshot
2007-07-16	Claudio Sacerdoti...	One daemon less.	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom