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

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

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
2007-11-25	Claudio Sacerdoti...	Bug fixed: an unification exception used to escape...	commit \| commitdiff \| tree
2007-11-23	Claudio Sacerdoti...	This alternative version of disambiguate.crit2 implements...	commit \| commitdiff \| tree
2007-11-22	Claudio Sacerdoti...	Bug fixed in printing of passes in error messages.	commit \| commitdiff \| tree
2007-11-21	Claudio Sacerdoti...	Very incomplete example of simple calculus exercises...	commit \| commitdiff \| tree
2007-11-19	Claudio Sacerdoti...	Bug fixed: local type declarations are not allowed...	commit \| commitdiff \| tree
2007-11-18	Claudio Sacerdoti...	The axiom can be proved. Just follow the hint.	commit \| commitdiff \| tree
2007-11-16	Claudio Sacerdoti...	Some notes for Enrico.	commit \| commitdiff \| tree
2007-11-14	Claudio Sacerdoti...	Bug fixed: yet another case where tys of mutual recursive...	commit \| commitdiff \| tree
2007-11-10	Claudio Sacerdoti...	a) Detection of existential types now implemented	commit \| commitdiff \| tree
2007-11-10	Claudio Sacerdoti...	More correct (but still bugged) implementation of type...	commit \| commitdiff \| tree
2007-11-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2007-11-08	Claudio Sacerdoti...	Trivial bug fixed in type inference of LetIn source...	commit \| commitdiff \| tree
2007-11-08	Claudio Sacerdoti...	Arguments of constructors in a case pattern are now...	commit \| commitdiff \| tree
2007-11-08	Claudio Sacerdoti...	svn:ignore set	commit \| commitdiff \| tree
2007-11-08	Claudio Sacerdoti...	Zoli's note (in Italian) about a constructive version...	commit \| commitdiff \| tree
2007-11-06	Claudio Sacerdoti...	cic_acic should be compiled before cic_exportation	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Bug in detection of too polymorphic types partially...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	MutCases that occur in types should be handled with...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Obj.magic are now generated to extract dependently...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Handling of left parameters of constructors/indutive...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Slightly nicer output.	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Filenames are now fully mangled (e.g. matita_nat_nat...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Type application and abstractions are now exported...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	New OCaml keyword "val".	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	"f" => "aux" to avoid name clashes	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	The type parameters in an inductive type declaration...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	Type arguments are better uncapitalized.	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	Empty types not in Prop and empty types elimination...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	Empty and singleton type elimination are now handled...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	1. type definitions of propositions are no longer exported...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	Bug fixed: qualified names were not generated correctly...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	* type definitions that define a new proposition are...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	CicExportation branched. Change "if false" with "if...	commit \| commitdiff \| tree
next

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

RSS Atom