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

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

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
2005-11-25	Claudio Sacerdoti...	More on the presentation.	commit \| commitdiff \| tree
2005-11-25	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-11-25	Claudio Sacerdoti...	Unused file removed.	commit \| commitdiff \| tree
2005-11-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-11-24	Claudio Sacerdoti...	Da capo (matita2.tex).	commit \| commitdiff \| tree
2005-11-23	Claudio Sacerdoti...	New implementation for localized exceptions.	commit \| commitdiff \| tree
2005-11-23	Claudio Sacerdoti...	* New implementation of localized exceptions	commit \| commitdiff \| tree
2005-11-23	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-11-23	Claudio Sacerdoti...	More on accessibility.	commit \| commitdiff \| tree
2005-11-22	Claudio Sacerdoti...	Debugging code commented out.	commit \| commitdiff \| tree
2005-11-22	Claudio Sacerdoti...	Error messages improved.	commit \| commitdiff \| tree
2005-11-22	Claudio Sacerdoti...	"Localization" of error messages for eat_prods and...	commit \| commitdiff \| tree
2005-11-22	Claudio Sacerdoti...	Less verbose error messages.	commit \| commitdiff \| tree
2005-11-22	Claudio Sacerdoti...	Last details.	commit \| commitdiff \| tree
2005-11-21	Claudio Sacerdoti...	Proof using function induction terminated. It's really...	commit \| commitdiff \| tree
2005-11-21	Claudio Sacerdoti...	Lost of redundant typing hints removed from the functional...	commit \| commitdiff \| tree
2005-11-21	Claudio Sacerdoti...	New proof based on an hand-made functional induction.	commit \| commitdiff \| tree
2005-11-21	Claudio Sacerdoti...	Useful lemma added.	commit \| commitdiff \| tree
2005-11-21	Claudio Sacerdoti...	Invariant no longer true (since when?)	commit \| commitdiff \| tree
2005-11-21	Claudio Sacerdoti...	More informative error messages.	commit \| commitdiff \| tree
2005-11-19	Claudio Sacerdoti...	"let rec f = ... in f l" used to be compiled incorrectly	commit \| commitdiff \| tree
2005-11-19	Claudio Sacerdoti...	Error messages improvement.	commit \| commitdiff \| tree
2005-11-19	Claudio Sacerdoti...	Less verbose error messages (= substitution applied...	commit \| commitdiff \| tree
2005-11-19	Claudio Sacerdoti...	Wrong reported error message fixed.	commit \| commitdiff \| tree
2005-11-19	Claudio Sacerdoti...	More information is now printed when reporting errors.	commit \| commitdiff \| tree
2005-11-19	Claudio Sacerdoti...	Typo fixed.	commit \| commitdiff \| tree
2005-11-19	Claudio Sacerdoti...	Disambiguation errors are no longer thrown away. They...	commit \| commitdiff \| tree
2005-11-19	Claudio Sacerdoti...	Coercions are now inserted also around the sources...	commit \| commitdiff \| tree
2005-11-18	Claudio Sacerdoti...	Incredible bug fixed: coercions were computed and then...	commit \| commitdiff \| tree
2005-11-18	Claudio Sacerdoti...	Improvement/bug fix: rewriting in the hypothesis used...	commit \| commitdiff \| tree
2005-11-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-11-17	Claudio Sacerdoti...	New test for parallel rewriting in the hypotheses and...	commit \| commitdiff \| tree
2005-11-17	Claudio Sacerdoti...	Comments changed/removed.	commit \| commitdiff \| tree
2005-11-17	Claudio Sacerdoti...	"Parallel" rewriting in a list of hypothesis and in...	commit \| commitdiff \| tree
2005-11-17	Claudio Sacerdoti...	Major code semplification and improvement:	commit \| commitdiff \| tree
2005-11-17	Claudio Sacerdoti...	First draft implementation of rewriting in an hypothesis.	commit \| commitdiff \| tree
2005-11-17	Claudio Sacerdoti...	New tactic rename (for now for internal usage only).	commit \| commitdiff \| tree
2005-11-17	Claudio Sacerdoti...	Inizio stesura parte su "libreria tutta visibile".	commit \| commitdiff \| tree
2005-11-17	Claudio Sacerdoti...	tests and tests.opt targets greately simplified	commit \| commitdiff \| tree
2005-11-16	Claudio Sacerdoti...	dump_moo.opt	commit \| commitdiff \| tree
2005-11-16	Claudio Sacerdoti...	do_test.sh no longer prints the compiler options (used...	commit \| commitdiff \| tree
2005-11-16	Claudio Sacerdoti...	New framework for regression of bad tests.	commit \| commitdiff \| tree
2005-11-16	Claudio Sacerdoti...	The .depend must not be committed! Fixed.	commit \| commitdiff \| tree
2005-11-15	Claudio Sacerdoti...	1. handling of tests and tests.opt targets improved	commit \| commitdiff \| tree
2005-11-15	Claudio Sacerdoti...	New directory for bad tests with checks on the error...	commit \| commitdiff \| tree
2005-11-15	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-11-15	Claudio Sacerdoti...	Debugging code commented out.	commit \| commitdiff \| tree
2005-11-15	Claudio Sacerdoti...	Bug fixed: wrong exception was raised (instead of returning...	commit \| commitdiff \| tree
2005-11-08	Claudio Sacerdoti...	Yet another semantics for simplify.	commit \| commitdiff \| tree
2005-11-08	Claudio Sacerdoti...	Yet another semantics for simplify.	commit \| commitdiff \| tree
2005-11-08	Claudio Sacerdoti...	CicTypeChecker.AssertFailure now printed.	commit \| commitdiff \| tree
2005-11-08	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree
2005-11-08	Claudio Sacerdoti...	New syntax for the outtype of a match.	commit \| commitdiff \| tree
2005-11-07	Claudio Sacerdoti...	Refinement of a Cast was bugged.	commit \| commitdiff \| tree
2005-11-07	Claudio Sacerdoti...	AssertFailure from the type-checker now becomes an...	commit \| commitdiff \| tree
2005-11-07	Claudio Sacerdoti...	Let-ins with types can now be produced.	commit \| commitdiff \| tree
2005-11-07	Claudio Sacerdoti...	Avoid generation of let x = let rec x = ... in x in...	commit \| commitdiff \| tree
2005-11-07	Claudio Sacerdoti...	Let-ins with types can be produced.	commit \| commitdiff \| tree
2005-11-07	Claudio Sacerdoti...	Syntactic change:	commit \| commitdiff \| tree
2005-11-07	Claudio Sacerdoti...	Syntactic change:	commit \| commitdiff \| tree
2005-11-07	Claudio Sacerdoti...	Duplicated exception definition removed (used to give...	commit \| commitdiff \| tree
2005-11-04	Claudio Sacerdoti...	matita.opt are now considered as if they were matita	commit \| commitdiff \| tree
2005-11-03	Claudio Sacerdoti...	Semantic change: I always consider a type with no constructo...	commit \| commitdiff \| tree
next

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

RSS Atom