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

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

2010-06-17	Enrico Tassi	off by one fixed	commit \| commitdiff \| tree \| snapshot
2010-06-10	Wilmer Ricciotti	Fix for inversion principles of types with a single...	commit \| commitdiff \| tree \| snapshot
2010-06-08	Wilmer Ricciotti	Fixed a bug in the undebruijnate function which caused...	commit \| commitdiff \| tree \| snapshot
2010-06-07	Enrico Tassi	some stuff on re	commit \| commitdiff \| tree \| snapshot
2010-06-07	Enrico Tassi	unify left args of inductive types with left argus...	commit \| commitdiff \| tree \| snapshot
2010-05-12	Wilmer Ricciotti	Library support files for John Major equality and Russell.	commit \| commitdiff \| tree \| snapshot
2010-05-12	Wilmer Ricciotti	Experimental support for Russell (coercions moving...	commit \| commitdiff \| tree \| snapshot
2010-05-11	Andrea Asperti	minimization.ma	commit \| commitdiff \| tree \| snapshot
2010-05-11	Enrico Tassi	little workaround for multiple screens, gdk support...	commit \| commitdiff \| tree \| snapshot
2010-05-10	Enrico Tassi	new intro:	commit \| commitdiff \| tree \| snapshot
2010-05-07	Enrico Tassi	trace generation with "// by _;"	commit \| commitdiff \| tree \| snapshot
2010-05-07	Enrico Tassi	notation	commit \| commitdiff \| tree \| snapshot
2010-05-07	Andrea Asperti	remarks and applyS	commit \| commitdiff \| tree \| snapshot
2010-05-06	Claudio Sacerdoti...	Bug fixed: nstatus => status (to undo the changes).	commit \| commitdiff \| tree \| snapshot
2010-05-06	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-05-06	Wilmer Ricciotti	Fixing naming scheme for composite coercions.	commit \| commitdiff \| tree \| snapshot
2010-05-06	Claudio Sacerdoti...	assert false could happen	commit \| commitdiff \| tree \| snapshot
2010-05-06	Claudio Sacerdoti...	Bug fixed:	commit \| commitdiff \| tree \| snapshot
2010-05-05	Claudio Sacerdoti...	coinduction is between us	commit \| commitdiff \| tree \| snapshot
2010-05-05	Claudio Sacerdoti...	First tests.	commit \| commitdiff \| tree \| snapshot
2010-05-04	Wilmer Ricciotti	* Fixed a couple of glitches in ndestruct	commit \| commitdiff \| tree \| snapshot
2010-05-04	Claudio Sacerdoti...	Regular expressions.	commit \| commitdiff \| tree \| snapshot
2010-04-21	Ferruccio Guidi	new dependences	commit \| commitdiff \| tree \| snapshot
2010-04-19	Andrea Asperti	Elimination of recursive inductive types leads to looping.	commit \| commitdiff \| tree \| snapshot
2010-04-19	Andrea Asperti	alpha_eq instead of pervasives.compare	commit \| commitdiff \| tree \| snapshot
2010-04-15	Enrico Tassi	bool_ext on 'o' not on 'Prop' (they are convertible...	commit \| commitdiff \| tree \| snapshot
2010-04-14	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-04-14	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-04-14	Claudio Sacerdoti...	Formal points.	commit \| commitdiff \| tree \| snapshot
2010-04-14	Claudio Sacerdoti...	Some dualization clean-up.	commit \| commitdiff \| tree \| snapshot
2010-04-13	Enrico Tassi	fixed makefile	commit \| commitdiff \| tree \| snapshot
2010-04-13	Enrico Tassi	auto destructs while introducing in the context	commit \| commitdiff \| tree \| snapshot
2010-04-13	Enrico Tassi	print nobjects (hack with Obj.magic)	commit \| commitdiff \| tree \| snapshot
2010-04-13	Enrico Tassi	catch the right exception, avoid uncaught Subst_not_found	commit \| commitdiff \| tree \| snapshot
2010-04-13	Enrico Tassi	same heads different arity -> INCOMPARABLE	commit \| commitdiff \| tree \| snapshot
2010-04-13	Enrico Tassi	some fixes to THF parser	commit \| commitdiff \| tree \| snapshot
2010-04-13	Enrico Tassi	fixed support file for TPTP	commit \| commitdiff \| tree \| snapshot
2010-04-11	Ferruccio Guidi	the edges must be quoted as well (not only the nodes)	commit \| commitdiff \| tree \| snapshot
2010-04-09	Andrea Asperti	apply_subst_context on statuses	commit \| commitdiff \| tree \| snapshot
2010-04-08	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2010-04-08	Enrico Tassi	support axioms	commit \| commitdiff \| tree \| snapshot
2010-04-08	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2010-04-08	Enrico Tassi	thf problems list for tptp 4.0.1	commit \| commitdiff \| tree \| snapshot
2010-04-08	Enrico Tassi	fixed compiltion order of lexer/parser	commit \| commitdiff \| tree \| snapshot
2010-04-08	Claudio Sacerdoti...	New code (unbranched) to compute all keys by all possib...	commit \| commitdiff \| tree \| snapshot
2010-04-08	Claudio Sacerdoti...	New sets of.	commit \| commitdiff \| tree \| snapshot
2010-04-08	Enrico Tassi	THF parser received some care	commit \| commitdiff \| tree \| snapshot
2010-04-08	Andrea Asperti	Fixing indexing (commit parziale di Claudio?)	commit \| commitdiff \| tree \| snapshot
2010-04-07	Enrico Tassi	THF parser for TPTP	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	Not is now inductive.	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	Use the inversion!	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	Bug fixed: the current equation is not always the last...	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	- inversion principles are now generated also for co...	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	More debugging info from print_tac.	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	Implicit and UserInput were printed incorrectly.	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	ninversion	commit \| commitdiff \| tree \| snapshot
2010-03-31	Andrea Asperti	removed boh	commit \| commitdiff \| tree \| snapshot
2010-03-31	Wilmer Ricciotti	Added test file for inversion in ng matita.	commit \| commitdiff \| tree \| snapshot
2010-03-31	Andrea Asperti	Tracing mechanism for auto. Interface changed to solve...	commit \| commitdiff \| tree \| snapshot
2010-03-26	Claudio Sacerdoti...	Good definition found.	commit \| commitdiff \| tree \| snapshot
2010-03-26	Claudio Sacerdoti...	(Co)Inductively Generated Formal Topologies (not only...	commit \| commitdiff \| tree \| snapshot
2010-03-25	Matthias Puech	patched the definition of locate, advances in locate_ad...	commit \| commitdiff \| tree \| snapshot
2010-03-25	Wilmer Ricciotti	Z.ma updated to reflect changes in the logical Not...	commit \| commitdiff \| tree \| snapshot
2010-03-25	Matthias Puech	Automation problem	commit \| commitdiff \| tree \| snapshot
2010-03-25	Andrea Asperti	More work	commit \| commitdiff \| tree \| snapshot
2010-03-25	Andrea Asperti	cosi va (se vi pare).	commit \| commitdiff \| tree \| snapshot
2010-03-25	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-25	Andrea Asperti	Conflict(?).	commit \| commitdiff \| tree \| snapshot
2010-03-25	Andrea Asperti	Extension of demod to arbtrary predicates (not just...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Nice examples for automation (that fails).	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Simplified proof after pattern fix	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	"Not" is no longer a definition	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	The precedence of ^-1 has changed.	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Equality has one right parameter and thus it's eliminat...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Real numbers as co-inductive streams of digits (overlap...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Andrea Asperti	Computation of the trace.	commit \| commitdiff \| tree \| snapshot
2010-03-23	Matthias Puech	typo in a proof	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	One more case.	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Readded eqf_2.	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	symmetric_eq -> sym_eq	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Re-proved an axiom	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Commented a few lemmas (copies).	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Fixed a few bugs	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	"flat" function (subst unfolding)	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Keeping only lift_aux e subst_aux (renamed to lift...	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Moved compare in a different file.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Matthias Puech	Downgrading level of infix notations involving \sup.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Porting alla nuova def. di negazione	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Nuova versione di not.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Printings removed.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Debugging disabled.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Debugging disabled.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	New demodulation tactics (mostly for debugging purposes).	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Exporting the demodulation function.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	New option "demod" for auto.	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom