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

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

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
2006-11-12	Claudio Sacerdoti...	The pretty printers in CicPp now have an optional ...	commit \| commitdiff \| tree
2006-11-05	Claudio Sacerdoti...	Some clean-up here and there in dama (coercions removed...	commit \| commitdiff \| tree
2006-11-05	Claudio Sacerdoti...	Almost every hand-inserted coercion removed since a...	commit \| commitdiff \| tree
2006-11-05	Claudio Sacerdoti...	Bug fixed: the disambiguation domain for a record with...	commit \| commitdiff \| tree
2006-11-05	Claudio Sacerdoti...	Critical bug finally found after a long chasing!!!	commit \| commitdiff \| tree
2006-11-05	Claudio Sacerdoti...	Added more typing information to remove a coercion.	commit \| commitdiff \| tree
2006-10-31	Claudio Sacerdoti...	The OK button of the disambiguation errors interface...	commit \| commitdiff \| tree
2006-10-31	Claudio Sacerdoti...	Bug fixed: inductive types were no longer removed from...	commit \| commitdiff \| tree
2006-10-31	Claudio Sacerdoti...	New behaviour of the disambiguation error messages...	commit \| commitdiff \| tree
2006-10-30	Claudio Sacerdoti...	TermAcicContent.Interpretation_not_found catched and...	commit \| commitdiff \| tree
2006-10-30	Claudio Sacerdoti...	Up to integration f-algebras.	commit \| commitdiff \| tree
2006-10-30	Claudio Sacerdoti...	Debugging code is now controlled by the debug flag.	commit \| commitdiff \| tree
2006-10-30	Claudio Sacerdoti...	remove_obj is now much faster:	commit \| commitdiff \| tree
2006-10-29	Claudio Sacerdoti...	Added target preall.opt.	commit \| commitdiff \| tree
2006-10-28	Claudio Sacerdoti...	GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion...	commit \| commitdiff \| tree
2006-10-26	Claudio Sacerdoti...	Better label for the disambiguation errors window.	commit \| commitdiff \| tree
2006-10-26	Claudio Sacerdoti...	New (and much more complex) disambiguation error interface.	commit \| commitdiff \| tree
2006-10-26	Claudio Sacerdoti...	More timeout added to autos here and there.	commit \| commitdiff \| tree
2006-10-25	Claudio Sacerdoti...	1. is_meta_closed should be applied only to terms on...	commit \| commitdiff \| tree
2006-10-25	Claudio Sacerdoti...	Added timeouts to auto here and there.	commit \| commitdiff \| tree
2006-10-25	Claudio Sacerdoti...	Added timeout to autos here and there.	commit \| commitdiff \| tree
2006-10-25	Claudio Sacerdoti...	1. bug fixed: Unicode characters that are not mapped...	commit \| commitdiff \| tree
2006-10-25	Claudio Sacerdoti...	/home/fguidi/... => ../../...	commit \| commitdiff \| tree
2006-10-25	Claudio Sacerdoti...	Our unification used to guess a very complex argument...	commit \| commitdiff \| tree
2006-10-25	Claudio Sacerdoti...	Two lemmas that used to pass no more now pass again...	commit \| commitdiff \| tree
2006-10-23	Claudio Sacerdoti...	Better (and more localized) error message for sort_of_prod.	commit \| commitdiff \| tree
2006-10-23	Claudio Sacerdoti...	CicUniv.UniverseInconsistency is no handled correcly.	commit \| commitdiff \| tree
2006-10-23	Claudio Sacerdoti...	binaries/saturate no longer compiled since it does...	commit \| commitdiff \| tree
2006-10-19	Claudio Sacerdoti...	Disambiguation errors are now compressed in a maybe...	commit \| commitdiff \| tree
2006-10-19	Claudio Sacerdoti...	Bug fixed: when trying to insert coercions after an...	commit \| commitdiff \| tree
2006-10-19	Claudio Sacerdoti...	Potential performance improvement + better disambiguation...	commit \| commitdiff \| tree
next

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

RSS Atom