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

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

2010-01-22	Cosimo Oliboni	freescale porting	commit \| commitdiff \| tree \| snapshot
2010-01-21	Cosimo Oliboni	(no commit message)	commit \| commitdiff \| tree \| snapshot
2010-01-21	Andrea Asperti	Esempio	commit \| commitdiff \| tree \| snapshot
2010-01-21	Cosimo Oliboni	(no commit message)	commit \| commitdiff \| tree \| snapshot
2010-01-21	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2010-01-19	Claudio Sacerdoti...	We can always use the "covered by emptyset" relation...	commit \| commitdiff \| tree \| snapshot
2010-01-18	Claudio Sacerdoti...	More //.	commit \| commitdiff \| tree \| snapshot
2010-01-18	Claudio Sacerdoti...	More // everywhere.	commit \| commitdiff \| tree \| snapshot
2010-01-18	Claudio Sacerdoti...	// used everywhere!	commit \| commitdiff \| tree \| snapshot
2010-01-18	Claudio Sacerdoti...	// in place of nauto everywhere	commit \| commitdiff \| tree \| snapshot
2010-01-18	Claudio Sacerdoti...	// is now more powerful	commit \| commitdiff \| tree \| snapshot
2010-01-18	Claudio Sacerdoti...	// is now more powerful	commit \| commitdiff \| tree \| snapshot
2010-01-18	Andrea Asperti	New paramod tac.	commit \| commitdiff \| tree \| snapshot
2010-01-18	Andrea Asperti	Invocation of paramod	commit \| commitdiff \| tree \| snapshot
2010-01-18	Andrea Asperti	paramod_tac exported	commit \| commitdiff \| tree \| snapshot
2010-01-18	Andrea Asperti	Number notation for NG	commit \| commitdiff \| tree \| snapshot
2010-01-18	Andrea Asperti	Number notation for NG	commit \| commitdiff \| tree \| snapshot
2010-01-18	Andrea Asperti	Number notation for NG.	commit \| commitdiff \| tree \| snapshot
2010-01-18	Andrea Asperti	Keeping Implicit for refinement (instead of transformin...	commit \| commitdiff \| tree \| snapshot
2010-01-18	Andrea Asperti	Updating.	commit \| commitdiff \| tree \| snapshot
2010-01-15	Claudio Sacerdoti...	A slightly more complicated example.	commit \| commitdiff \| tree \| snapshot
2010-01-15	Claudio Sacerdoti...	Finished!	commit \| commitdiff \| tree \| snapshot
2010-01-15	Claudio Sacerdoti...	We are still equivalent (even if the definition of...	commit \| commitdiff \| tree \| snapshot
2010-01-15	Claudio Sacerdoti...	Urrah!	commit \| commitdiff \| tree \| snapshot
2010-01-15	Claudio Sacerdoti...	Extending to the nAx set.	commit \| commitdiff \| tree \| snapshot
2010-01-15	Claudio Sacerdoti...	Skipfact function (a partial general recursive function...	commit \| commitdiff \| tree \| snapshot
2010-01-12	Wilmer Ricciotti	Fixed a bug in the discrimination principle: the refine...	commit \| commitdiff \| tree \| snapshot
2010-01-11	Claudio Sacerdoti...	Finished	commit \| commitdiff \| tree \| snapshot
2010-01-11	Andrea Asperti	1. New paramodulation function	commit \| commitdiff \| tree \| snapshot
2010-01-11	Andrea Asperti	saturate cust be called with delta=0	commit \| commitdiff \| tree \| snapshot
2010-01-11	Andrea Asperti	Added is_equation	commit \| commitdiff \| tree \| snapshot
2010-01-11	Andrea Asperti	Debugging info	commit \| commitdiff \| tree \| snapshot
2010-01-08	Claudio Sacerdoti...	Improved	commit \| commitdiff \| tree \| snapshot
2010-01-08	Claudio Sacerdoti...	Partial porting to new syntax.	commit \| commitdiff \| tree \| snapshot
2010-01-08	Claudio Sacerdoti...	Source language path must be appended, not replaced.	commit \| commitdiff \| tree \| snapshot
2010-01-08	Claudio Sacerdoti...	Categorical stuff postponed.	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	The body of constants is a reference, not the actual...	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	removed debugging info	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	applyS	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	refresh uri	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	Support for the new auto tactics //	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	Support for the new // tactics.	commit \| commitdiff \| tree \| snapshot
2010-01-08	Andrea Asperti	new reloc_subst (to avoid cyclic substitutions).	commit \| commitdiff \| tree \| snapshot
2010-01-07	Enrico Tassi	....	commit \| commitdiff \| tree \| snapshot
2010-01-07	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2010-01-07	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2010-01-06	Claudio Sacerdoti...	Simplified.	commit \| commitdiff \| tree \| snapshot
2010-01-06	Claudio Sacerdoti...	Coercions via unification hints?	commit \| commitdiff \| tree \| snapshot
2010-01-05	Ferruccio Guidi	- we now add the kernel options in the preamble of...	commit \| commitdiff \| tree \| snapshot
2010-01-02	Claudio Sacerdoti...	1) stuff moved from categories.ma to setoids*.ma	commit \| commitdiff \| tree \| snapshot
2009-12-30	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-12-30	Claudio Sacerdoti...	Almost done (up to definition of category).	commit \| commitdiff \| tree \| snapshot
2009-12-30	Claudio Sacerdoti...	Porting of Sambin's stuff started.	commit \| commitdiff \| tree \| snapshot
2009-12-30	Claudio Sacerdoti...	Porting of Sambin's stuff started.	commit \| commitdiff \| tree \| snapshot
2009-12-30	Claudio Sacerdoti...	Removed line is back again.	commit \| commitdiff \| tree \| snapshot
2009-12-30	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-12-21	Andrea Asperti	Refining with no expected type + unification seems...	commit \| commitdiff \| tree \| snapshot
2009-12-21	Andrea Asperti	Trying to be faster	commit \| commitdiff \| tree \| snapshot
2009-12-21	Andrea Asperti	Trying to be faster.	commit \| commitdiff \| tree \| snapshot
2009-12-18	Andrea Asperti	Final subst returned by superposition and passed around.	commit \| commitdiff \| tree \| snapshot
2009-12-18	Andrea Asperti	using = instead of alpha conversions. context metasenv...	commit \| commitdiff \| tree \| snapshot
2009-12-15	Andrea Asperti	eq_coerc for smart application.	commit \| commitdiff \| tree \| snapshot
2009-12-14	Ferruccio Guidi	the sort hierarchy parameter enter the kernel status	commit \| commitdiff \| tree \| snapshot
2009-12-10	Andrea Asperti	Minor bag fixed, relative to failures.	commit \| commitdiff \| tree \| snapshot
2009-12-10	Andrea Asperti	A compiling version?	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added a "sort_metasenv" function.	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Commented a couple of calls to "set_reference_of_oxuri".	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added the paramodulation stuff to the status	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	param "slir" to call the new auto	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added the paramodulation active/passive tables to the...	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Attached fast_eq_check to auto	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added nnAuto.mli	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Debug set to ()	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Clean up of debgging info	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Syntax error	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Wrong reference corrected	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Minor fixing for last chance	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added a fol operation	commit \| commitdiff \| tree \| snapshot
2009-12-04	Wilmer Ricciotti	Bugfix in inversion (was using refl_eq instead of refl).	commit \| commitdiff \| tree \| snapshot
2009-12-04	Andrea Asperti	Indexing local context for paramod.	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Propositional equality	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	The new paramodulation functions instantiated over...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	New ways for initialising the signature required for...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Passive equations have their own index (not passive...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	debug takes lazy strings. Moved here the are_alpha_eq...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Added a function remove_unit_clause	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Added a boolean test function to discriminate equations...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Generalized intitialization for EqP	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Generalized initialization of eqP.	commit \| commitdiff \| tree \| snapshot
2009-12-01	Enrico Tassi	porting to lablgtk2 >= 2.14 and releasing	commit \| commitdiff \| tree \| snapshot
2009-12-01	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-11-27	Wilmer Ricciotti	ndestruct now clears off identity equations whenever...	commit \| commitdiff \| tree \| snapshot
2009-11-25	Wilmer Ricciotti	Fixed inversion, which was broken by the last changes...	commit \| commitdiff \| tree \| snapshot
2009-11-25	Andrea Asperti	Exported forward_inference_step	commit \| commitdiff \| tree \| snapshot
2009-11-24	Wilmer Ricciotti	Bugfix in tipify: a metavariable was set to type withou...	commit \| commitdiff \| tree \| snapshot
2009-11-24	Wilmer Ricciotti	In order to prevent useless meta extensions, we optimiz...	commit \| commitdiff \| tree \| snapshot
2009-11-24	Wilmer Ricciotti	When unifying	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom