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

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

2011-05-26	Claudio Sacerdoti...	Added "nocomposites" to coercions.	commit \| commitdiff \| tree \| snapshot
2011-05-25	Ferruccio Guidi	- degree: some improvements and the Deg_append lemma	commit \| commitdiff \| tree \| snapshot
2011-05-24	Claudio Sacerdoti...	Quick patch to avoid name collisions when passing coerc...	commit \| commitdiff \| tree \| snapshot
2011-05-24	Claudio Sacerdoti...	Coercions are now propagated under let...ins.	commit \| commitdiff \| tree \| snapshot
2011-05-24	Wilmer Ricciotti	Fixed box pretty printing.	commit \| commitdiff \| tree \| snapshot
2011-05-24	Wilmer Ricciotti	matitaweb: added retract (undo)	commit \| commitdiff \| tree \| snapshot
2011-05-24	Ferruccio Guidi	degree.ma: we defined the "degree" of a term, which...	commit \| commitdiff \| tree \| snapshot
2011-05-23	Claudio Sacerdoti...	1) interpretation of matches in patterns implemented	commit \| commitdiff \| tree \| snapshot
2011-05-23	Wilmer Ricciotti	Added support for hyperlinks in the goal view of the...	commit \| commitdiff \| tree \| snapshot
2011-05-23	Wilmer Ricciotti	...	commit \| commitdiff \| tree \| snapshot
2011-05-23	Andrea Asperti	Removed dead code	commit \| commitdiff \| tree \| snapshot
2011-05-20	Ferruccio Guidi	- we weakened SAT3	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	want_indent bug fixed	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	readded function box_of	commit \| commitdiff \| tree \| snapshot
2011-05-20	Wilmer Ricciotti	Compilation fix	commit \| commitdiff \| tree \| snapshot
2011-05-20	Wilmer Ricciotti	Compilation fix	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	Simplified rendering.	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	Simplified rendering	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	Simplified rendering	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	rm rendering attrs	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	Removed mathml and proof rendering.	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	Simplified rendering	commit \| commitdiff \| tree \| snapshot
2011-05-20	Andrea Asperti	Porting to new reduction.	commit \| commitdiff \| tree \| snapshot
2011-05-19	Wilmer Ricciotti	Added matitadaemon.	commit \| commitdiff \| tree \| snapshot
2011-05-19	Ferruccio Guidi	cube.ma: some pts specifications of the lambda-cube	commit \| commitdiff \| tree \| snapshot
2011-05-19	Andrea Asperti	Porting to the new pts.	commit \| commitdiff \| tree \| snapshot
2011-05-19	Andrea Asperti	Porting to new parametric TJ.	commit \| commitdiff \| tree \| snapshot
2011-05-19	Andrea Asperti	Dummies are blocked.	commit \| commitdiff \| tree \| snapshot
2011-05-18	Andrea Asperti	New version of TJ parametric in the specification of...	commit \| commitdiff \| tree \| snapshot
2011-05-14	Ferruccio Guidi	we added a property	commit \| commitdiff \| tree \| snapshot
2011-05-13	Ferruccio Guidi	ground: some arithmetical properties added	commit \| commitdiff \| tree \| snapshot
2011-05-13	Wilmer Ricciotti	interim version (added smallLexer)	commit \| commitdiff \| tree \| snapshot
2011-05-12	Wilmer Ricciotti	Record projections:	commit \| commitdiff \| tree \| snapshot
2011-05-12	Wilmer Ricciotti	Record projections:	commit \| commitdiff \| tree \| snapshot
2011-05-11	Andrea Asperti	Partial modifications.	commit \| commitdiff \| tree \| snapshot
2011-04-28	Ferruccio Guidi	we uncommented R3 and R4 tu be used in lambda-delta	commit \| commitdiff \| tree \| snapshot
2011-04-28	Ferruccio Guidi	- weight: bugfix + weight-based eliminator axiomatized	commit \| commitdiff \| tree \| snapshot
2011-04-21	Ferruccio Guidi	- we added notation for the zetable and thetable items	commit \| commitdiff \| tree \| snapshot
2011-04-20	Andrea Asperti	convertibility.	commit \| commitdiff \| tree \| snapshot
2011-04-20	Andrea Asperti	generatin lemmas and subject reduction (with a lot...	commit \| commitdiff \| tree \| snapshot
2011-04-20	Andrea Asperti	progress	commit \| commitdiff \| tree \| snapshot
2011-04-20	Andrea Asperti	error in the conversion rule	commit \| commitdiff \| tree \| snapshot
2011-04-19	Ferruccio Guidi	notation bug fix	commit \| commitdiff \| tree \| snapshot
2011-04-19	Ferruccio Guidi	- some bug fixes	commit \| commitdiff \| tree \| snapshot
2011-04-19	Ferruccio Guidi	complete reformalization of lambda-delta in matita...	commit \| commitdiff \| tree \| snapshot
2011-04-19	Ferruccio Guidi	disambiguation of explicit interprettions with argument...	commit \| commitdiff \| tree \| snapshot
2011-04-13	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2011-04-05	Ferruccio Guidi	we added an nmap from NCic.obj to NotationPt.obj (to...	commit \| commitdiff \| tree \| snapshot
2011-04-05	Ferruccio Guidi	we removed an extra dot from the "include" syntax	commit \| commitdiff \| tree \| snapshot
2011-04-04	Ferruccio Guidi	we introduced nterm for NotationPt.term	commit \| commitdiff \| tree \| snapshot
2011-04-01	Claudio Sacerdoti...	Patch to avoid equations of the form ? -> T (oriented...	commit \| commitdiff \| tree \| snapshot
2011-03-30	Ferruccio Guidi	we proved that the union of two saturated sets is saturated	commit \| commitdiff \| tree \| snapshot
2011-03-30	Wilmer Ricciotti	Keeping track of locations of disambiguated ids and...	commit \| commitdiff \| tree \| snapshot
2011-03-27	Claudio Sacerdoti...	Fixes previous wrong commit.	commit \| commitdiff \| tree \| snapshot
2011-03-27	Claudio Sacerdoti...	1) Second half of the bug fixing for the "lexical keywo...	commit \| commitdiff \| tree \| snapshot
2011-03-27	Claudio Sacerdoti...	Bug fixed: some Uri was not refreshed. The effect of...	commit \| commitdiff \| tree \| snapshot
2011-03-27	Claudio Sacerdoti...	Debugging code commented out.	commit \| commitdiff \| tree \| snapshot
2011-03-23	Ferruccio Guidi	- terms.ma: we included 'is_dummy" and "neutral" (maybe...	commit \| commitdiff \| tree \| snapshot
2011-03-23	Claudio Sacerdoti...	More verbose in case of errors.	commit \| commitdiff \| tree \| snapshot
2011-03-23	Andrea Asperti	red star	commit \| commitdiff \| tree \| snapshot
2011-03-23	Claudio Sacerdoti...	Use jmeq from lib.	commit \| commitdiff \| tree \| snapshot
2011-03-23	Claudio Sacerdoti...	Nested calls to matitac are now pretty-printed nicely.	commit \| commitdiff \| tree \| snapshot
2011-03-22	Claudio Sacerdoti...	Reindentation.	commit \| commitdiff \| tree \| snapshot
2011-03-22	Ferruccio Guidi	the weakening lemma is not needed since it is assumed...	commit \| commitdiff \| tree \| snapshot
2011-03-22	Ferruccio Guidi	the thinning lemma follows immediately from the substit...	commit \| commitdiff \| tree \| snapshot
2011-03-22	Ferruccio Guidi	- lambda_notation.ma: more notation and bug fixes	commit \| commitdiff \| tree \| snapshot
2011-03-22	Claudio Sacerdoti...	Bug fixed and code refactoring: now both matitac and...	commit \| commitdiff \| tree \| snapshot
2011-03-22	Claudio Sacerdoti...	Use matita/lib as the new standard library in place...	commit \| commitdiff \| tree \| snapshot
2011-03-22	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2011-03-21	Andrea Asperti	sn_prod	commit \| commitdiff \| tree \| snapshot
2011-03-21	Andrea Asperti	sn_lambda	commit \| commitdiff \| tree \| snapshot
2011-03-21	Andrea Asperti	extensions	commit \| commitdiff \| tree \| snapshot
2011-03-19	Claudio Sacerdoti...	Bug "fixed" (i.e avoided).	commit \| commitdiff \| tree \| snapshot
2011-03-18	Claudio Sacerdoti...	Ported to	commit \| commitdiff \| tree \| snapshot
2011-03-15	Ferruccio Guidi	- more notation and service lemmas	commit \| commitdiff \| tree \| snapshot
2011-03-15	Ferruccio Guidi	- some ignores	commit \| commitdiff \| tree \| snapshot
2011-03-14	Ferruccio Guidi	dependences fix	commit \| commitdiff \| tree \| snapshot
2011-03-11	Andrea Asperti	added star.ma (star closure of a relation)	commit \| commitdiff \| tree \| snapshot
2011-03-11	Andrea Asperti	Improvements.	commit \| commitdiff \| tree \| snapshot
2011-03-10	Andrea Asperti	diamond property	commit \| commitdiff \| tree \| snapshot
2011-03-09	Ferruccio Guidi	more notation and all-purpose lemmas	commit \| commitdiff \| tree \| snapshot
2011-03-09	Ferruccio Guidi	the interpretation for Sigma was missing	commit \| commitdiff \| tree \| snapshot
2011-03-08	Wilmer Ricciotti	First commit with new (incomplete) disambiguation engine.	commit \| commitdiff \| tree \| snapshot
2011-03-07	Andrea Asperti	sottotermini e confluenza (manca pr_substs).	commit \| commitdiff \| tree \| snapshot
2011-03-02	Ferruccio Guidi	we started the implementation of higher order saturated...	commit \| commitdiff \| tree \| snapshot
2011-02-27	Ferruccio Guidi	- rc_sat.ma: we changed the notation for extensional...	commit \| commitdiff \| tree \| snapshot
2011-02-27	Ferruccio Guidi	- notation is now in a separate file	commit \| commitdiff \| tree \| snapshot
2011-02-26	Ferruccio Guidi	- new file ext.ma with the objects needed for the norma...	commit \| commitdiff \| tree \| snapshot
2011-02-21	Ferruccio Guidi	we started to set up the strong normalization proof.	commit \| commitdiff \| tree \| snapshot
2011-02-21	Wilmer Ricciotti	fork for Matita version B	commit \| commitdiff \| tree \| snapshot
2011-02-10	Ferruccio Guidi	we added some comments	commit \| commitdiff \| tree \| snapshot
2011-02-10	Andrea Asperti	Added typing rule for dummies	commit \| commitdiff \| tree \| snapshot
2011-02-10	Andrea Asperti	Added lambda	commit \| commitdiff \| tree \| snapshot
2011-02-09	Wilmer Ricciotti	enabling destruct defs	commit \| commitdiff \| tree \| snapshot
2011-01-27	Claudio Sacerdoti...	Hyperlinks are back.	commit \| commitdiff \| tree \| snapshot
2011-01-27	Claudio Sacerdoti...	Hyperlinks are now computed correctly. I least I hope...	commit \| commitdiff \| tree \| snapshot
2011-01-21	Wilmer Ricciotti	Removed inclusion of logic/equality.ma in datatypes...	commit \| commitdiff \| tree \| snapshot
2011-01-20	Wilmer Ricciotti	Bugfix for elimination principles.	commit \| commitdiff \| tree \| snapshot
2011-01-20	Wilmer Ricciotti	Bug fix for generation of elimination principles.	commit \| commitdiff \| tree \| snapshot
2011-01-19	Wilmer Ricciotti	Added some typing info to elimination principles, allow...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom