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

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

2008-04-08	Claudio Sacerdoti...	Variables having a body can occur in cooked terms and...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Fix over the previous one: Var-LetIn abstractions should...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Error message improved.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Cooking w.r.t. variables with bodies is now implemented...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Fix name capture in cofix.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	To test the translation.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Name capture fixed.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Improved error messages in place of "sort elimination...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Seed reset before each convert_obj.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Use seed to avoid further name clashes.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Incredible, but true! Our name mangling clashed with...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Cooked objects are no longer well typed in the uncooked...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Improved eat_prods error message (at the cost of passing...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	The old kernel does not accept ens whose order is different...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Bad alpha-conversion by Enrico fixed.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Bug fixed: the ens need not be ordered w.r.t. the declared...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	j off by one in error message	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	fix_outty partially fixed: missing lifts in args and ens	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	fix_outty fixed in order to perform eta-expansion when...	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Tentative (and bad!) fix of outtypes in non-dependent...	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Cooking discriminated into cooking in types (using...	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Pretty-printing of definitions fixed.	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Cooking implemented (not tested yet).	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Reports improved.	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Debugging code fixed.	commit \| commitdiff \| tree
2008-04-01	Claudio Sacerdoti...	typeof_obj0 implemented	commit \| commitdiff \| tree
2008-04-01	Claudio Sacerdoti...	1) added get_checked_indtys that returns the whole...	commit \| commitdiff \| tree
2008-03-31	Claudio Sacerdoti...	Automatic generation of elimination and inversion principles...	commit \| commitdiff \| tree
2008-03-31	Claudio Sacerdoti...	Large amount of duplicated code (still in comments...	commit \| commitdiff \| tree
2008-03-31	Claudio Sacerdoti...	1) Impredicative sort "Set" removed everywhere.	commit \| commitdiff \| tree
2008-03-31	Claudio Sacerdoti...	1) more sharing everywhere in NCicSubstitution	commit \| commitdiff \| tree
2008-03-20	Claudio Sacerdoti...	New syntax for auto-related tactics and conclude/obtain.	commit \| commitdiff \| tree
2008-03-20	Claudio Sacerdoti...	Script fixed (it did not compile due to a mistake before...	commit \| commitdiff \| tree
2008-03-20	Claudio Sacerdoti...	End of patch for computation of LetIn types. Now types...	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	Bug: types and terms pushed into the context must be...	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	-debug improved	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	prerr_endline => debug_print	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	prerr_endline => debug_print	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	Number notation for Coq is back again, waiting for...	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	Files committed by Enrico (a mistake, I suppose) removed.	commit \| commitdiff \| tree
2008-03-14	Claudio Sacerdoti...	Tests enabled again.	commit \| commitdiff \| tree
2008-03-13	Claudio Sacerdoti...	:-(	commit \| commitdiff \| tree
2008-03-13	Claudio Sacerdoti...	New version of freescale:	commit \| commitdiff \| tree
2008-03-12	Claudio Sacerdoti...	Problem solved (was: apply needed an argument to avoid...	commit \| commitdiff \| tree
2008-03-12	Claudio Sacerdoti...	Almost always correct optimization: during unification...	commit \| commitdiff \| tree
2008-03-11	Claudio Sacerdoti...	Very experimental commit: the type of the source is...	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Bad hack to avoid failure of conversion (unfolding...	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Scripts fixed because of:	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Tactic reduce got rid of. Use normalize, instead.	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	whd: ~delta=false now controls also zeta-reduction...	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	An unimplemented case of clearbody is now implemented.	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	check_metasenv_consistency:	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Example query fixed.	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Debugging print removed.	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Added ad-hoc optimization for check_metasenv_consistency...	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Performance improvement: let-ins should always be pushed...	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Scripts fixed. They were broken since the change to...	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Potentially (and, at least sometimes, actually) big...	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Redundant check (because of an invariant) removed.	commit \| commitdiff \| tree
2008-03-04	Claudio Sacerdoti...	New syntax for patterns.	commit \| commitdiff \| tree
2008-03-04	Claudio Sacerdoti...	prodT ==> prod	commit \| commitdiff \| tree
2008-03-04	Claudio Sacerdoti...	A) New version.	commit \| commitdiff \| tree
2008-02-21	Claudio Sacerdoti...	A new very simple example for recursive functions....	commit \| commitdiff \| tree
2008-02-21	Claudio Sacerdoti...	Avoid translating back recursive fixes to the same...	commit \| commitdiff \| tree
2008-02-21	Claudio Sacerdoti...	Avoid application to 0 arguments.	commit \| commitdiff \| tree
2008-02-21	Claudio Sacerdoti...	Better handling of exceptions.	commit \| commitdiff \| tree
2008-02-08	Claudio Sacerdoti...	A formalization of modified realisability with truth...	commit \| commitdiff \| tree
2008-02-08	Claudio Sacerdoti...	Bug fixed in generation of elimination principles of...	commit \| commitdiff \| tree
2008-02-08	Claudio Sacerdoti...	prodT merged with prod	commit \| commitdiff \| tree
2008-02-07	Claudio Sacerdoti...	ProdT was a perfect copy of Prod. Removed.	commit \| commitdiff \| tree
2008-01-21	Claudio Sacerdoti...	Matitac now accepts multiple targets :-) (but only...	commit \| commitdiff \| tree
2008-01-21	Claudio Sacerdoti...	Hack for code extraction re-linked, but disactivated.	commit \| commitdiff \| tree
2008-01-21	Claudio Sacerdoti...	Old tiny freescale experiment get rid of.	commit \| commitdiff \| tree
2008-01-21	Claudio Sacerdoti...	Typo fixed.	commit \| commitdiff \| tree
2007-12-16	Claudio Sacerdoti...	Much more verbose statistics.	commit \| commitdiff \| tree
2007-12-16	Claudio Sacerdoti...	Bug fixed: \n prevented recognition.	commit \| commitdiff \| tree
2007-12-05	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2007-12-04	Claudio Sacerdoti...	Repeated errors are not duplicated.	commit \| commitdiff \| tree
2007-12-04	Claudio Sacerdoti...	Even if the error is not localized, it was not a good...	commit \| commitdiff \| tree
2007-12-04	Claudio Sacerdoti...	Some terms are not localized from the very beginning :-(	commit \| commitdiff \| tree
2007-12-04	Claudio Sacerdoti...	Added debugging option to ask for all disambiguation...	commit \| commitdiff \| tree
2007-12-04	Claudio Sacerdoti...	One more error localized. But the code is really ugly...	commit \| commitdiff \| tree
2007-12-04	Claudio Sacerdoti...	Only errors from passes 4 and 6 are kept.	commit \| commitdiff \| tree
2007-12-04	Claudio Sacerdoti...	Reindented.	commit \| commitdiff \| tree
2007-12-02	Claudio Sacerdoti...	Forward compatibility with new lablgtk2.	commit \| commitdiff \| tree
2007-11-28	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2007-11-28	Claudio Sacerdoti...	Bug fixed: an unification exception used to escape...	commit \| commitdiff \| tree
2007-11-27	Claudio Sacerdoti...	Output is now in UTF8 character counts.	commit \| commitdiff \| tree
2007-11-27	Claudio Sacerdoti...	Options declared but not parsed.	commit \| commitdiff \| tree
2007-11-27	Claudio Sacerdoti...	Ported to camlp5 < 5.00	commit \| commitdiff \| tree
2007-11-27	Claudio Sacerdoti...	Back-ported to camlp5 < 5.00.	commit \| commitdiff \| tree
2007-11-26	Claudio Sacerdoti...	Axiom moved from ex_deriv to deriv where it belongs to.	commit \| commitdiff \| tree
2007-11-26	Claudio Sacerdoti...	Notation improved.	commit \| commitdiff \| tree
2007-11-26	Claudio Sacerdoti...	Some code clean-up.	commit \| commitdiff \| tree
2007-11-26	Claudio Sacerdoti...	Disambiguation error compaction is now performed in...	commit \| commitdiff \| tree
2007-11-26	Claudio Sacerdoti...	Patch to automatically generate filename.error.md5...	commit \| commitdiff \| tree
2007-11-25	Claudio Sacerdoti...	This version of disambiguate.ml implements yet another...	commit \| commitdiff \| tree
next

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

RSS Atom