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

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

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
2007-07-16	Claudio Sacerdoti...	More daemons got rid of (and more extra axioms to be...	commit \| commitdiff \| tree \| snapshot
2007-07-16	Claudio Sacerdoti...	Last daemon killed :-)	commit \| commitdiff \| tree \| snapshot
2007-07-16	Claudio Sacerdoti...	One less daemon (about "update"s).	commit \| commitdiff \| tree \| snapshot
2007-07-16	Claudio Sacerdoti...	All sub-proofs about "update" closed.	commit \| commitdiff \| tree \| snapshot
2007-07-16	Claudio Sacerdoti...	assembly.ma splitted into many files	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	* NOT RELEASED YET	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	* NOT RELEASED YET	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	proper path for ps.gz doc	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	texlive-base-bin, texlive-latex-extra	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	- add build-dep for doc generation: graphviz, texlive...	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	- add build-dep for doc generation: graphviz, texlive...	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	* debian/rules	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	invoke make doc after build to create ocamldoc docs	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	* debian/svn-deblayout	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	* rebuild against OCaml 3.10 and ocamlnet 2.2	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	* debian/*.install.in	commit \| commitdiff \| tree \| snapshot
2007-07-16	Stefano Zacchiroli	* rebuild with OCaml 3.10	commit \| commitdiff \| tree \| snapshot
2007-07-16	Wilmer Ricciotti	corrected axiom mod_plus	commit \| commitdiff \| tree \| snapshot
2007-07-14	Ferruccio Guidi	new definitions and new theorems	commit \| commitdiff \| tree \| snapshot
2007-07-13	Claudio Sacerdoti...	More conjectures closed.	commit \| commitdiff \| tree \| snapshot
2007-07-13	Claudio Sacerdoti...	1. requires the new pretty printer for natural numbers	commit \| commitdiff \| tree \| snapshot
2007-07-13	Claudio Sacerdoti...	Dirty patch by Zack: natural numbers of Matita are...	commit \| commitdiff \| tree \| snapshot
2007-07-13	Claudio Sacerdoti...	Last crazy commit reverted.	commit \| commitdiff \| tree \| snapshot
2007-07-13	Claudio Sacerdoti...	Final theorem proved. Many many conjectures left. I...	commit \| commitdiff \| tree \| snapshot
2007-07-12	Claudio Sacerdoti...	The loop invariant I chosed was not correct!	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom