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

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

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
2006-12-12	Ferruccio Guidi	we parametrized CicNotationPt.obj on 'term	commit \| commitdiff \| tree \| snapshot
2006-12-12	Ferruccio Guidi	we started the infrastructure for the procedural render...	commit \| commitdiff \| tree \| snapshot
2006-12-09	Ferruccio Guidi	we exported some inversors from coq	commit \| commitdiff \| tree \| snapshot
2006-12-08	Claudio Sacerdoti...	EXPERIMENTAL:	commit \| commitdiff \| tree \| snapshot
2006-12-08	Claudio Sacerdoti...	Disambiguation errors in phase 3 that are not present...	commit \| commitdiff \| tree \| snapshot
2006-12-08	Ferruccio Guidi	new makefiles	commit \| commitdiff \| tree \| snapshot
2006-12-07	Stefano Zacchiroli	reverted error committed by mistake	commit \| commitdiff \| tree \| snapshot
2006-12-07	Stefano Zacchiroli	avoid Failure "nth" when only one disambiguation pass...	commit \| commitdiff \| tree \| snapshot
2006-12-07	Ferruccio Guidi	new theorems added. does not comile well yet :(( proble...	commit \| commitdiff \| tree \| snapshot
2006-12-06	Claudio Sacerdoti...	Experimental: cycles in proofs generated by paramodulat...	commit \| commitdiff \| tree \| snapshot
2006-12-06	Claudio Sacerdoti...	More simplification using better notation.	commit \| commitdiff \| tree \| snapshot
2006-12-06	Claudio Sacerdoti...	interactive and bad_tests grepped out before insertion...	commit \| commitdiff \| tree \| snapshot
2006-12-05	Stefano Zacchiroli	experimental classification of disambiguation error...	commit \| commitdiff \| tree \| snapshot
2006-12-05	Ferruccio Guidi	- components: composed coercions mus be generated with...	commit \| commitdiff \| tree \| snapshot
2006-12-05	Stefano Zacchiroli	do not share the db connection among children, should...	commit \| commitdiff \| tree \| snapshot
2006-12-01	Ferruccio Guidi	prova.ma: baseuri fixed	commit \| commitdiff \| tree \| snapshot
2006-12-01	Ferruccio Guidi	some uris fixed	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	Even if automatically generated, I prefer to commit...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	Notation \middot used everywhere in place of *.	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	I have changed the nice notation for derivatives a...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	Added a demo for Matita: two slightly different proofs...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	Syntax of a declarative rewritinstep changed.	commit \| commitdiff \| tree \| snapshot
2006-11-30	Wilmer Ricciotti	library/Fsub: minor fix	commit \| commitdiff \| tree \| snapshot
2006-11-30	Wilmer Ricciotti	library: added solution to POPLMark challenge part...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	New syntax and semantics for the rewriting steps that...	commit \| commitdiff \| tree \| snapshot
2006-11-30	Claudio Sacerdoti...	The auto parameters that can be given to a declarative...	commit \| commitdiff \| tree \| snapshot
2006-11-29	Claudio Sacerdoti...	The rewritingstep declarative command now takes also...	commit \| commitdiff \| tree \| snapshot
2006-11-29	Ferruccio Guidi	- new library/logic/coimplication.ma uses new decompose...	commit \| commitdiff \| tree \| snapshot
2006-11-29	Ferruccio Guidi	- decompose tactic: decomposable constants are now...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom