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

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

2006-01-27	Claudio Sacerdoti...	1. The last commit that fixed unification of compound...	commit \| commitdiff \| tree
2006-01-27	Claudio Sacerdoti...	A few paramodulation/demodulation tests moved from...	commit \| commitdiff \| tree
2006-01-27	Claudio Sacerdoti...	Big bug fixed: attributes of constants were forgot...	commit \| commitdiff \| tree
2006-01-27	Claudio Sacerdoti...	Cambiamenti nella parte sulla disambiguazione.	commit \| commitdiff \| tree
2006-01-26	Claudio Sacerdoti...	A failing unification of a coercion vs a term is now...	commit \| commitdiff \| tree
2006-01-25	Claudio Sacerdoti...	New formulation of finite_enumerable_SemiGroups to...	commit \| commitdiff \| tree
2006-01-25	Claudio Sacerdoti...	First part of a slightly more interesting proof on...	commit \| commitdiff \| tree
2006-01-25	Claudio Sacerdoti...	6hands-introduction to the last two sections	commit \| commitdiff \| tree
2006-01-23	Claudio Sacerdoti...	right and left cancellation in groups	commit \| commitdiff \| tree
2006-01-23	Claudio Sacerdoti...	Cenni alla disambiguazione lazy.	commit \| commitdiff \| tree
2006-01-20	Claudio Sacerdoti...	Yet another strategy for let...ins: a let-in is _NEVER_...	commit \| commitdiff \| tree
2006-01-19	Claudio Sacerdoti...	New reduction strategy (that behaves much better during...	commit \| commitdiff \| tree
2006-01-19	Claudio Sacerdoti...	1. Back to nicer (and more comprehensible) notation...	commit \| commitdiff \| tree
2006-01-19	Claudio Sacerdoti...	"Hiding" notation for implicit coercion. Cool.	commit \| commitdiff \| tree
2006-01-19	Claudio Sacerdoti...	A few experiments (with horrible results) using notation...	commit \| commitdiff \| tree
2006-01-18	Claudio Sacerdoti...	Aggiornato alla nuova gerarchia di moduli.	commit \| commitdiff \| tree
2006-01-18	Claudio Sacerdoti...	library ==> component	commit \| commitdiff \| tree
2006-01-18	Claudio Sacerdoti...	paramodulation is no longer a self-alone module	commit \| commitdiff \| tree
2006-01-18	Claudio Sacerdoti...	baseuri of coq.ma fixed	commit \| commitdiff \| tree
2006-01-18	Claudio Sacerdoti...	libraries.ps no longer in synch.	commit \| commitdiff \| tree
2006-01-18	Claudio Sacerdoti...	New dependencies!	commit \| commitdiff \| tree
2006-01-17	Claudio Sacerdoti...	Bug fixed (in Cast).	commit \| commitdiff \| tree
2006-01-17	Claudio Sacerdoti...	An embryonic kernel of the algebraic library.	commit \| commitdiff \| tree
2006-01-17	Claudio Sacerdoti...	subst_vars optimized for the explicit_named_subst=...	commit \| commitdiff \| tree
2006-01-16	Claudio Sacerdoti...	Dead code removed and reindentation.	commit \| commitdiff \| tree
2006-01-16	Claudio Sacerdoti...	(Partial commit)	commit \| commitdiff \| tree
2006-01-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2006-01-16	Claudio Sacerdoti...	Bug fixed: the wrong context was used.	commit \| commitdiff \| tree
2006-01-16	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-13	Claudio Sacerdoti...	More informative error message.	commit \| commitdiff \| tree
2006-01-12	Claudio Sacerdoti...	ignore used to avoid Y warning	commit \| commitdiff \| tree
2006-01-12	Claudio Sacerdoti...	Dependency coq.moo.opt added to target tests.opt	commit \| commitdiff \| tree
2006-01-12	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-12	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-11	Claudio Sacerdoti...	svn now uses $SVNOPTIONS;	commit \| commitdiff \| tree
2006-01-11	Claudio Sacerdoti...	New table bench_svn to keep the map "mark"==>"revision"	commit \| commitdiff \| tree
2006-01-11	Claudio Sacerdoti...	Hand-made generated inversion lemma.	commit \| commitdiff \| tree
2006-01-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-10	Claudio Sacerdoti...	Warning Y fixed.	commit \| commitdiff \| tree
2006-01-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2006-01-09	Claudio Sacerdoti...	paramodulation now compiles with ocaml 3.09 in opt...	commit \| commitdiff \| tree
2006-01-09	Claudio Sacerdoti...	The proofContext method now returns the empty context...	commit \| commitdiff \| tree
2006-01-09	Claudio Sacerdoti...	Bug fixed in computation of the domain of records with...	commit \| commitdiff \| tree
2006-01-09	Claudio Sacerdoti...	Bux fixed: matita did not save the .lexicon files!...	commit \| commitdiff \| tree
2006-01-09	Claudio Sacerdoti...	$Id$ readded to paramodulation/utils.ml	commit \| commitdiff \| tree
2006-01-09	Claudio Sacerdoti...	Stupid bug of mine fixed: sometimes (Some ~-1) was...	commit \| commitdiff \| tree
2006-01-09	Claudio Sacerdoti...	New version.	commit \| commitdiff \| tree
2006-01-08	Claudio Sacerdoti...	Bug fixed: the include_paths were no longer handled...	commit \| commitdiff \| tree
2006-01-08	Claudio Sacerdoti...	Bug fixed: macros in the middle of a goto cursor or...	commit \| commitdiff \| tree
2006-01-08	Claudio Sacerdoti...	Added $Id$ to every .ml file.	commit \| commitdiff \| tree
2006-01-08	Claudio Sacerdoti...	Added $Id$ to the file.	commit \| commitdiff \| tree
2006-01-08	Claudio Sacerdoti...	.cvsignore files removed (the svn:property property...	commit \| commitdiff \| tree
2006-01-08	Claudio Sacerdoti...	1. Macros are now handled using an execption that is...	commit \| commitdiff \| tree
2005-12-22	Claudio Sacerdoti...	Added parameter first_statement_only to the functions...	commit \| commitdiff \| tree
2005-12-22	Claudio Sacerdoti...	alias diffing/insertion is now handled by matitaEngine...	commit \| commitdiff \| tree
2005-12-22	Claudio Sacerdoti...	Makefiles made less verbose.	commit \| commitdiff \| tree
2005-12-21	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-12-21	Claudio Sacerdoti...	Huge reorganization of matita and ocaml.	commit \| commitdiff \| tree
2005-12-21	Claudio Sacerdoti...	Huge reorganization of matita and ocaml.	commit \| commitdiff \| tree
2005-12-09	Claudio Sacerdoti...	Bug fixed: errors of phase 7 were no longer printed :-)	commit \| commitdiff \| tree
2005-12-09	Claudio Sacerdoti...	1. useless code (undebrujin) removed from disambiguate.ml	commit \| commitdiff \| tree
2005-12-07	Claudio Sacerdoti...	More compact disambiguation errors.	commit \| commitdiff \| tree
2005-12-07	Claudio Sacerdoti...	The last commit about coercions disactivated localization...	commit \| commitdiff \| tree
2005-12-05	Claudio Sacerdoti...	eval_from_stream_greedy finally got rid of!	commit \| commitdiff \| tree
2005-12-05	Claudio Sacerdoti...	1. Several files in grafite that should be in grafite_parser...	commit \| commitdiff \| tree
2005-12-05	Claudio Sacerdoti...	1. Several files in grafite that should be in grafite_parser...	commit \| commitdiff \| tree
2005-12-03	Claudio Sacerdoti...	metadata are no longer stored in .moo files.	commit \| commitdiff \| tree
2005-12-03	Claudio Sacerdoti...	1. metadata are no longer stored in .moo files.	commit \| commitdiff \| tree
2005-12-02	Claudio Sacerdoti...	1. matitaEngine splitted into disambiguation (now in...	commit \| commitdiff \| tree
2005-12-02	Claudio Sacerdoti...	1. matitaEngine splitted into disambiguation (now in...	commit \| commitdiff \| tree
2005-11-30	Claudio Sacerdoti...	moved coercion to library (work in progress)	commit \| commitdiff \| tree
2005-11-30	Claudio Sacerdoti...	moved coercions away (work in progress)	commit \| commitdiff \| tree
2005-11-30	Claudio Sacerdoti...	coercGraph.ml* moved from cic_unification to library	commit \| commitdiff \| tree
2005-11-30	Claudio Sacerdoti...	Implicit aliases are now defined as all the aliases...	commit \| commitdiff \| tree
2005-11-30	Claudio Sacerdoti...	nicer (but convertible) types	commit \| commitdiff \| tree
2005-11-30	Claudio Sacerdoti...	* Undo fixed.	commit \| commitdiff \| tree
2005-11-30	Claudio Sacerdoti...	Terms parsed by notations were not localized.	commit \| commitdiff \| tree
2005-11-30	Claudio Sacerdoti...	Generation of auxiliary lemmas for inductive types...	commit \| commitdiff \| tree
2005-11-29	Claudio Sacerdoti...	* Part of matita that used to deal with the library...	commit \| commitdiff \| tree
2005-11-28	Claudio Sacerdoti...	* More error messages localized.	commit \| commitdiff \| tree
2005-11-28	Claudio Sacerdoti...	More errors localized.	commit \| commitdiff \| tree
2005-11-28	Claudio Sacerdoti...	More error messages localized.	commit \| commitdiff \| tree
2005-11-28	Claudio Sacerdoti...	More aggressive politic for non localized terms: an...	commit \| commitdiff \| tree
2005-11-28	Claudio Sacerdoti...	DisambiguationError exceptions (that have locations...	commit \| commitdiff \| tree
2005-11-28	Claudio Sacerdoti...	1. Bug fixed: compilation of "let corec" to a simple...	commit \| commitdiff \| tree
2005-11-26	Claudio Sacerdoti...	* wrong comments removed	commit \| commitdiff \| tree
2005-11-26	Claudio Sacerdoti...	Refinement bug fixed. The outtype was not refined if...	commit \| commitdiff \| tree
2005-11-26	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree
2005-11-26	Claudio Sacerdoti...	Bug fixed: an unrefined term was passed around while...	commit \| commitdiff \| tree
2005-11-26	Claudio Sacerdoti...	Experimental localization of errors during refinement...	commit \| commitdiff \| tree
2005-11-26	Claudio Sacerdoti...	Module CicHash (hash-tables over CIC terms based on...	commit \| commitdiff \| tree
2005-11-25	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-11-25	Claudio Sacerdoti...	Non exhaustive match fixed.	commit \| commitdiff \| tree
2005-11-25	Claudio Sacerdoti...	Confronto con Coq.	commit \| commitdiff \| tree
2005-11-25	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-11-25	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
next

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

RSS Atom