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

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

2007-05-23	Claudio Sacerdoti...	Automatic exploration of the theory of intuitionistic...	commit \| commitdiff \| tree
2007-05-22	Claudio Sacerdoti...	Slightly more efficient patch.	commit \| commitdiff \| tree
2007-05-18	Claudio Sacerdoti...	In some cases (e.g. JM equality) the inversion principle...	commit \| commitdiff \| tree
2007-04-24	Claudio Sacerdoti...	goal ==> focus	commit \| commitdiff \| tree
2007-04-23	Claudio Sacerdoti...	Deprecated "goal" removed.	commit \| commitdiff \| tree
2007-04-20	Claudio Sacerdoti...	A new test on some non punctuation tacticals.	commit \| commitdiff \| tree
2007-04-20	Claudio Sacerdoti...	The declarative rewriting step now tries auto timeout...	commit \| commitdiff \| tree
2007-04-20	Claudio Sacerdoti...	added skip, removed end	commit \| commitdiff \| tree
2007-04-20	Claudio Sacerdoti...	Much ado about nothing:	commit \| commitdiff \| tree
2007-04-20	Claudio Sacerdoti...	Bug fixed: off by one array access in the last patch.	commit \| commitdiff \| tree
2007-04-20	Claudio Sacerdoti...	Interface of the argument to Continuationals.Make greately...	commit \| commitdiff \| tree
2007-04-19	Claudio Sacerdoti...	EXPERIMENTAL and _INCOMPLETE_ COMMIT:	commit \| commitdiff \| tree
2007-04-19	Claudio Sacerdoti...	The night test now shows the last commits and blames...	commit \| commitdiff \| tree
2007-04-18	Claudio Sacerdoti...	New query result diff.	commit \| commitdiff \| tree
2007-04-18	Claudio Sacerdoti...	Only benches with the same result are compared for...	commit \| commitdiff \| tree
2007-04-18	Claudio Sacerdoti...	Added new query to time-diff the last mark with the...	commit \| commitdiff \| tree
2007-04-18	Claudio Sacerdoti...	tassi/sacerdot	commit \| commitdiff \| tree
2007-03-26	Claudio Sacerdoti...	Serious bug fixed: a variable was captured during unfolding...	commit \| commitdiff \| tree
2007-03-22	Claudio Sacerdoti...	Several instances of the same bug fixed at once: when...	commit \| commitdiff \| tree
2007-03-22	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree
2007-03-13	Claudio Sacerdoti...	Role of	commit \| commitdiff \| tree
2007-02-09	Claudio Sacerdoti...	Avoid generating invalid names with "'" in the middle...	commit \| commitdiff \| tree
2007-02-09	Claudio Sacerdoti...	The ApplyTransformation.txt_of_term function has been...	commit \| commitdiff \| tree
2007-02-09	Claudio Sacerdoti...	Exceptions should never escape the final exception...	commit \| commitdiff \| tree
2007-02-09	Claudio Sacerdoti...	Debugging code fixed. To enable debugging just set...	commit \| commitdiff \| tree
2007-02-09	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree
2007-02-08	Claudio Sacerdoti...	More progress in technicalities/setoids.ma.	commit \| commitdiff \| tree
2007-02-08	Claudio Sacerdoti...	Manual for the "default" command updated.	commit \| commitdiff \| tree
2007-02-08	Claudio Sacerdoti...	* 'default "equality"' command changed to consider...	commit \| commitdiff \| tree
2007-02-08	Claudio Sacerdoti...	If a pretty printed term spans on multiple lines, then...	commit \| commitdiff \| tree
2007-02-08	Claudio Sacerdoti...	Important commit:	commit \| commitdiff \| tree
2007-02-07	Claudio Sacerdoti...	New dependency over acic_procedural.	commit \| commitdiff \| tree
2007-02-06	Claudio Sacerdoti...	More stuff in technicalities/setoids.ma	commit \| commitdiff \| tree
2007-02-06	Claudio Sacerdoti...	Debugging deactivated.	commit \| commitdiff \| tree
2007-02-06	Claudio Sacerdoti...	Bug fixed in the computation of the disambiguation...	commit \| commitdiff \| tree
2007-02-06	Claudio Sacerdoti...	Incredible bug fixed in Fix and CoFix. The types of...	commit \| commitdiff \| tree
2007-02-05	Claudio Sacerdoti...	Second formulation of a constructive (positive) proof...	commit \| commitdiff \| tree
2007-02-02	Claudio Sacerdoti...	Serious bug fixed: the types of a real mutual fix definition...	commit \| commitdiff \| tree
2007-01-31	Claudio Sacerdoti...	Several bugs fixed:	commit \| commitdiff \| tree
2007-01-31	Claudio Sacerdoti...	New test for mutual recursive definitions.	commit \| commitdiff \| tree
2007-01-30	Claudio Sacerdoti...	Proof size nicely reduced using distributive branching...	commit \| commitdiff \| tree
2007-01-30	Claudio Sacerdoti...	Even more (painful) work on setoids.	commit \| commitdiff \| tree
2007-01-30	Claudio Sacerdoti...	Behaviour of CicRefine.type_of_aux' on MutCases changed...	commit \| commitdiff \| tree
2007-01-29	Claudio Sacerdoti...	More work on setoids.	commit \| commitdiff \| tree
2007-01-29	Claudio Sacerdoti...	Some more datatypes lifted to Type.	commit \| commitdiff \| tree
2007-01-27	Claudio Sacerdoti...	Added option datatype. Required (for technicalities...	commit \| commitdiff \| tree
2007-01-26	Claudio Sacerdoti...	"Warning/error/debug/infos" messages now sent on stderr.	commit \| commitdiff \| tree
2007-01-26	Claudio Sacerdoti...	Some changes:	commit \| commitdiff \| tree
2007-01-20	Claudio Sacerdoti...	Just a few lines test to understand with Cezary Kalinsky...	commit \| commitdiff \| tree
2007-01-20	Claudio Sacerdoti...	Bug fixed: if the context of a sequent was empty a...	commit \| commitdiff \| tree
2007-01-20	Claudio Sacerdoti...	Added new function txt_of_cic_sequent.	commit \| commitdiff \| tree
2007-01-20	Claudio Sacerdoti...	1. buf fixed in eval_from_stream when first_statemente_only...	commit \| commitdiff \| tree
2007-01-20	Claudio Sacerdoti...	An "assert false" used to be raised when matitac was...	commit \| commitdiff \| tree
2007-01-17	Claudio Sacerdoti...	CoRN (new version) has been committed by Andrea in...	commit \| commitdiff \| tree
2007-01-07	Claudio Sacerdoti...	Porting of setoids.ma from Coq continued.	commit \| commitdiff \| tree
2007-01-07	Claudio Sacerdoti...	Bug fixed in definition of cic:/.../setoids/make_compatibili...	commit \| commitdiff \| tree
2007-01-03	Claudio Sacerdoti...	Notation is finally fully working everywhere.	commit \| commitdiff \| tree
2007-01-03	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree
2007-01-03	Claudio Sacerdoti...	Riesz_spaces are now seen as lattices + vector spaces...	commit \| commitdiff \| tree
2007-01-02	Claudio Sacerdoti...	There used to be two minimal joins between an ordered_set...	commit \| commitdiff \| tree
2007-01-02	Claudio Sacerdoti...	Same fix of the previous commit, but in a different...	commit \| commitdiff \| tree
2007-01-02	Claudio Sacerdoti...	1. More debugging code	commit \| commitdiff \| tree
2006-12-30	Claudio Sacerdoti...	Some more notation can now be used.	commit \| commitdiff \| tree
2006-12-30	Claudio Sacerdoti...	le x y ==> x \leq y (now possible because of a bug...	commit \| commitdiff \| tree
2006-12-30	Claudio Sacerdoti...	Serious bug fixed: arities of coercions in the .moo...	commit \| commitdiff \| tree
2006-12-29	Claudio Sacerdoti...	Record with simulated manifest types are now used everywhere in	commit \| commitdiff \| tree
2006-12-29	Claudio Sacerdoti...	First attempt at using/simulating records with manifest...	commit \| commitdiff \| tree
2006-12-29	Claudio Sacerdoti...	eq_ind' generalized to eq_rect'	commit \| commitdiff \| tree
2006-12-28	Claudio Sacerdoti...	Yet another localization error in eat_prods fixed.	commit \| commitdiff \| tree
2006-12-28	Claudio Sacerdoti...	.depends committed to fix non-compilation errors	commit \| commitdiff \| tree
2006-12-20	Claudio Sacerdoti...	New declarative tactic "we proceed by cases on t to...	commit \| commitdiff \| tree
2006-12-20	Claudio Sacerdoti...	Bug fixed in cases (it did not produced the right number...	commit \| commitdiff \| tree
2006-12-20	Claudio Sacerdoti...	Tactic cases documented	commit \| commitdiff \| tree
2006-12-20	Claudio Sacerdoti...	New tactic cases (still to be documented).	commit \| commitdiff \| tree
2006-12-18	Claudio Sacerdoti...	An idea to implement manifest record fields:	commit \| commitdiff \| tree
2006-12-15	Claudio Sacerdoti...	Huge DAMA update:	commit \| commitdiff \| tree
2006-12-14	Claudio Sacerdoti...	Bugged code patched, but not in the optimal way.	commit \| commitdiff \| tree
2006-12-14	Claudio Sacerdoti...	Debugging code commented out.	commit \| commitdiff \| tree
2006-12-14	Claudio Sacerdoti...	Huge commit:	commit \| commitdiff \| tree
2006-12-08	Claudio Sacerdoti...	EXPERIMENTAL:	commit \| commitdiff \| tree
2006-12-08	Claudio Sacerdoti...	Disambiguation errors in phase 3 that are not present...	commit \| commitdiff \| tree
2006-12-06	Claudio Sacerdoti...	Experimental: cycles in proofs generated by paramodulation...	commit \| commitdiff \| tree
2006-12-06	Claudio Sacerdoti...	More simplification using better notation.	commit \| commitdiff \| tree
2006-12-06	Claudio Sacerdoti...	interactive and bad_tests grepped out before insertion...	commit \| commitdiff \| tree
2006-11-30	Claudio Sacerdoti...	Even if automatically generated, I prefer to commit...	commit \| commitdiff \| tree
2006-11-30	Claudio Sacerdoti...	Notation \middot used everywhere in place of *.	commit \| commitdiff \| tree
2006-11-30	Claudio Sacerdoti...	I have changed the nice notation for derivatives a...	commit \| commitdiff \| tree
2006-11-30	Claudio Sacerdoti...	Added a demo for Matita: two slightly different proofs...	commit \| commitdiff \| tree
2006-11-30	Claudio Sacerdoti...	Syntax of a declarative rewritinstep changed.	commit \| commitdiff \| tree
2006-11-30	Claudio Sacerdoti...	New syntax and semantics for the rewriting steps that...	commit \| commitdiff \| tree
2006-11-30	Claudio Sacerdoti...	The auto parameters that can be given to a declarative...	commit \| commitdiff \| tree
2006-11-29	Claudio Sacerdoti...	The rewritingstep declarative command now takes also...	commit \| commitdiff \| tree
2006-11-28	Claudio Sacerdoti...	Added a clear to rewritestep to speed up auto (by removing...	commit \| commitdiff \| tree
2006-11-27	Claudio Sacerdoti...	"the thesis becomes" now always performs a change.	commit \| commitdiff \| tree
2006-11-27	Claudio Sacerdoti...	Fixed bug in notation: when a notation is applied to...	commit \| commitdiff \| tree
2006-11-27	Claudio Sacerdoti...	Declarative language ported to new auto (with Universes).	commit \| commitdiff \| tree
2006-11-27	Claudio Sacerdoti...	auto new => auto new library in those tests that use...	commit \| commitdiff \| tree
2006-11-17	Claudio Sacerdoti...	Fixed the infamous bug:	commit \| commitdiff \| tree
2006-11-14	Claudio Sacerdoti...	&TODO => &TODO;	commit \| commitdiff \| tree
2006-11-14	Claudio Sacerdoti...	library=1 in obtain _ = _ by _.	commit \| commitdiff \| tree
next

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

RSS Atom