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

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

2007-01-31	Claudio Sacerdoti...	Several bugs fixed:	commit \| commitdiff \| tree \| snapshot
2007-01-31	Claudio Sacerdoti...	New test for mutual recursive definitions.	commit \| commitdiff \| tree \| snapshot
2007-01-30	Claudio Sacerdoti...	Proof size nicely reduced using distributive branching...	commit \| commitdiff \| tree \| snapshot
2007-01-30	Claudio Sacerdoti...	Even more (painful) work on setoids.	commit \| commitdiff \| tree \| snapshot
2007-01-30	Claudio Sacerdoti...	Behaviour of CicRefine.type_of_aux' on MutCases changed...	commit \| commitdiff \| tree \| snapshot
2007-01-29	Claudio Sacerdoti...	More work on setoids.	commit \| commitdiff \| tree \| snapshot
2007-01-29	Claudio Sacerdoti...	Some more datatypes lifted to Type.	commit \| commitdiff \| tree \| snapshot
2007-01-29	Stefano Zacchiroli	well-formed ocamldoc comment	commit \| commitdiff \| tree \| snapshot
2007-01-29	Stefano Zacchiroli	preliminary cookie support	commit \| commitdiff \| tree \| snapshot
2007-01-27	Claudio Sacerdoti...	Added option datatype. Required (for technicalities...	commit \| commitdiff \| tree \| snapshot
2007-01-26	Claudio Sacerdoti...	"Warning/error/debug/infos" messages now sent on stderr.	commit \| commitdiff \| tree \| snapshot
2007-01-26	Claudio Sacerdoti...	Some changes:	commit \| commitdiff \| tree \| snapshot
2007-01-24	Ferruccio Guidi	tactics.mli: regenerated	commit \| commitdiff \| tree \| snapshot
2007-01-24	Ferruccio Guidi	matitaGui: some missing cases during disambiguation...	commit \| commitdiff \| tree \| snapshot
2007-01-24	Stefano Zacchiroli	send internally generated headers in lowercase form...	commit \| commitdiff \| tree \| snapshot
2007-01-22	Ferruccio Guidi	some patches	commit \| commitdiff \| tree \| snapshot
2007-01-20	Claudio Sacerdoti...	Just a few lines test to understand with Cezary Kalinsk...	commit \| commitdiff \| tree \| snapshot
2007-01-20	Claudio Sacerdoti...	Bug fixed: if the context of a sequent was empty a...	commit \| commitdiff \| tree \| snapshot
2007-01-20	Claudio Sacerdoti...	Added new function txt_of_cic_sequent.	commit \| commitdiff \| tree \| snapshot
2007-01-20	Claudio Sacerdoti...	1. buf fixed in eval_from_stream when first_statemente_...	commit \| commitdiff \| tree \| snapshot
2007-01-20	Claudio Sacerdoti...	An "assert false" used to be raised when matitac was...	commit \| commitdiff \| tree \| snapshot
2007-01-19	Ferruccio Guidi	some updates	commit \| commitdiff \| tree \| snapshot
2007-01-19	Ferruccio Guidi	Unified: refactoring	commit \| commitdiff \| tree \| snapshot
2007-01-18	Ferruccio Guidi	Unified: refactoring	commit \| commitdiff \| tree \| snapshot
2007-01-18	Ferruccio Guidi	Unified refactoring	commit \| commitdiff \| tree \| snapshot
2007-01-18	Ferruccio Guidi	Unified: refactoring	commit \| commitdiff \| tree \| snapshot
2007-01-18	Wilmer Ricciotti	new version, using new tacticals	commit \| commitdiff \| tree \| snapshot
2007-01-17	Enrico Zoli	This is the roadmap of the constructive proof of Lebesg...	commit \| commitdiff \| tree \| snapshot
2007-01-17	Claudio Sacerdoti...	CoRN (new version) has been committed by Andrea in...	commit \| commitdiff \| tree \| snapshot
2007-01-16	Andrea Asperti	Added SetoidInc.m	commit \| commitdiff \| tree \| snapshot
2007-01-16	Andrea Asperti	Some CoRN files.	commit \| commitdiff \| tree \| snapshot
2007-01-12	Ferruccio Guidi	procedural: added fwd rewrite in arbitrary proofs ...	commit \| commitdiff \| tree \| snapshot
2007-01-10	Ferruccio Guidi	procedural: buggy ast renderer fixed	commit \| commitdiff \| tree \| snapshot
2007-01-10	Ferruccio Guidi	attributes now in the proof status: commit 4	commit \| commitdiff \| tree \| snapshot
2007-01-10	Ferruccio Guidi	attributes now in the proof status: commit 3	commit \| commitdiff \| tree \| snapshot
2007-01-10	Ferruccio Guidi	attributes now in the proof status: commit 2	commit \| commitdiff \| tree \| snapshot
2007-01-10	Ferruccio Guidi	attributes now in the proof status: commit 1	commit \| commitdiff \| tree \| snapshot
2007-01-07	Claudio Sacerdoti...	Porting of setoids.ma from Coq continued.	commit \| commitdiff \| tree \| snapshot
2007-01-07	Claudio Sacerdoti...	Bug fixed in definition of cic:/.../setoids/make_compat...	commit \| commitdiff \| tree \| snapshot
2007-01-06	Enrico Tassi	- inside dicrimination_tree is now checked the invarian...	commit \| commitdiff \| tree \| snapshot
2007-01-06	Enrico Tassi	;auto fixed	commit \| commitdiff \| tree \| snapshot
2007-01-05	Enrico Tassi	removed debugging printing	commit \| commitdiff \| tree \| snapshot
2007-01-05	Enrico Tassi	debuggin message improved	commit \| commitdiff \| tree \| snapshot
2007-01-05	Enrico Tassi	add_moo_content does not add a coercion statement twice	commit \| commitdiff \| tree \| snapshot
2007-01-05	Enrico Tassi	Added check for duplicate (convertible) composite coerc...	commit \| commitdiff \| tree \| snapshot
2007-01-05	Enrico Tassi	Erroneously declared coercion removed	commit \| commitdiff \| tree \| snapshot
2007-01-03	Stefano Zacchiroli	ready for ocamlnet 2.2	commit \| commitdiff \| tree \| snapshot
2007-01-03	Stefano Zacchiroli	more elegant handling of all/opt building	commit \| commitdiff \| tree \| snapshot
2007-01-03	Claudio Sacerdoti...	Notation is finally fully working everywhere.	commit \| commitdiff \| tree \| snapshot
2007-01-03	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2007-01-03	Claudio Sacerdoti...	Riesz_spaces are now seen as lattices + vector spaces...	commit \| commitdiff \| tree \| snapshot
2007-01-03	Enrico Tassi	oder tests	commit \| commitdiff \| tree \| snapshot
2007-01-02	Claudio Sacerdoti...	There used to be two minimal joins between an ordered_s...	commit \| commitdiff \| tree \| snapshot
2007-01-02	Claudio Sacerdoti...	Same fix of the previous commit, but in a different...	commit \| commitdiff \| tree \| snapshot
2007-01-02	Claudio Sacerdoti...	1. More debugging code	commit \| commitdiff \| tree \| snapshot
2007-01-02	Enrico Tassi	added oblivion_universe and used it in paxck_coercions	commit \| commitdiff \| tree \| snapshot
2006-12-31	Ferruccio Guidi	some tests patched	commit \| commitdiff \| tree \| snapshot
2006-12-30	Claudio Sacerdoti...	Some more notation can now be used.	commit \| commitdiff \| tree \| snapshot
2006-12-30	Claudio Sacerdoti...	le x y ==> x \leq y (now possible because of a bug...	commit \| commitdiff \| tree \| snapshot
2006-12-30	Claudio Sacerdoti...	Serious bug fixed: arities of coercions in the .moo...	commit \| commitdiff \| tree \| snapshot
2006-12-30	Ferruccio Guidi	dependence to legacy/coq.ma fixed	commit \| commitdiff \| tree \| snapshot
2006-12-29	Ferruccio Guidi	now we try two distinct depend files for compilation...	commit \| commitdiff \| tree \| snapshot
2006-12-29	Claudio Sacerdoti...	Record with simulated manifest types are now used every...	commit \| commitdiff \| tree \| snapshot
2006-12-29	Claudio Sacerdoti...	First attempt at using/simulating records with manifest...	commit \| commitdiff \| tree \| snapshot
2006-12-29	Claudio Sacerdoti...	eq_ind' generalized to eq_rect'	commit \| commitdiff \| tree \| snapshot
2006-12-29	Ferruccio Guidi	- tactics:	commit \| commitdiff \| tree \| snapshot
2006-12-28	Claudio Sacerdoti...	Yet another localization error in eat_prods fixed.	commit \| commitdiff \| tree \| snapshot
2006-12-28	Claudio Sacerdoti...	.depends committed to fix non-compilation errors	commit \| commitdiff \| tree \| snapshot
2006-12-24	Ferruccio Guidi	some depend files	commit \| commitdiff \| tree \| snapshot
2006-12-22	Ferruccio Guidi	legacy development created	commit \| commitdiff \| tree \| snapshot
2006-12-22	Ferruccio Guidi	- sc3/props.ma sc3/arity.ma: dependences fixed	commit \| commitdiff \| tree \| snapshot
2006-12-22	Andrea Asperti	Add_moo_content modified to avoid repetitions of index...	commit \| commitdiff \| tree \| snapshot
2006-12-22	Andrea Asperti	Minor change.	commit \| commitdiff \| tree \| snapshot
2006-12-22	Andrea Asperti	Collapse_head_metas transforms all terms "not-recongniz...	commit \| commitdiff \| tree \| snapshot
2006-12-22	Andrea Asperti	In the let-in case we compute the type and add it to...	commit \| commitdiff \| tree \| snapshot
2006-12-22	Andrea Asperti	The function uri_of_term now works also if the explciit...	commit \| commitdiff \| tree \| snapshot
2006-12-22	Enrico Tassi	Speeedup! (by caching)	commit \| commitdiff \| tree \| snapshot
2006-12-21	Enrico Tassi	added some missing includes	commit \| commitdiff \| tree \| snapshot
2006-12-20	Claudio Sacerdoti...	New declarative tactic "we proceed by cases on t to...	commit \| commitdiff \| tree \| snapshot
2006-12-20	Claudio Sacerdoti...	Bug fixed in cases (it did not produced the right numbe...	commit \| commitdiff \| tree \| snapshot
2006-12-20	Claudio Sacerdoti...	Tactic cases documented	commit \| commitdiff \| tree \| snapshot
2006-12-20	Claudio Sacerdoti...	New tactic cases (still to be documented).	commit \| commitdiff \| tree \| snapshot
2006-12-20	Ferruccio Guidi	Procedural: method "Apply" ok in forward style	commit \| commitdiff \| tree \| snapshot
2006-12-19	Ferruccio Guidi	Procedural: "ByInduction" method ok	commit \| commitdiff \| tree \| snapshot
2006-12-18	Claudio Sacerdoti...	An idea to implement manifest record fields:	commit \| commitdiff \| tree \| snapshot
2006-12-18	Ferruccio Guidi	Procedural: some improvements	commit \| commitdiff \| tree \| snapshot
2006-12-18	Andrea Asperti	M logic/coimplication.ma	commit \| commitdiff \| tree \| snapshot
2006-12-18	Andrea Asperti	Renamed iterative into map_iter_p and moved around...	commit \| commitdiff \| tree \| snapshot
2006-12-18	Andrea Asperti	Proof of Euler theorem.	commit \| commitdiff \| tree \| snapshot
2006-12-15	Enrico Zoli	Up to definition of limsup as liminf computed on the...	commit \| commitdiff \| tree \| snapshot
2006-12-15	Enrico Zoli	Fatou lemma achieved (up to a few more axioms here...	commit \| commitdiff \| tree \| snapshot
2006-12-15	Claudio Sacerdoti...	Huge DAMA update:	commit \| commitdiff \| tree \| snapshot
2006-12-14	Claudio Sacerdoti...	Bugged code patched, but not in the optimal way.	commit \| commitdiff \| tree \| snapshot
2006-12-14	Claudio Sacerdoti...	Debugging code commented out.	commit \| commitdiff \| tree \| snapshot
2006-12-14	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2006-12-14	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2006-12-14	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2006-12-14	Ferruccio Guidi	content2Procedural.ml: "Intros+LetTac" ok	commit \| commitdiff \| tree \| snapshot
2006-12-14	Claudio Sacerdoti...	Huge commit:	commit \| commitdiff \| tree \| snapshot
2006-12-13	Ferruccio Guidi	- transcript: patched to generate aliases instead of...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom