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

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

2007-02-09	Stefano Zacchiroli	Added toggle for enabling/disabling the conversion...	commit \| commitdiff \| tree \| snapshot
2007-02-09	Claudio Sacerdoti...	The ApplyTransformation.txt_of_term function has been...	commit \| commitdiff \| tree \| snapshot
2007-02-09	Stefano Zacchiroli	- moved to the view menu toggles for coercion hiding...	commit \| commitdiff \| tree \| snapshot
2007-02-09	Claudio Sacerdoti...	Exceptions should never escape the final exception...	commit \| commitdiff \| tree \| snapshot
2007-02-09	Claudio Sacerdoti...	Debugging code fixed. To enable debugging just set...	commit \| commitdiff \| tree \| snapshot
2007-02-09	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2007-02-09	Stefano Zacchiroli	moved the high level pretty printing setting to a toggl...	commit \| commitdiff \| tree \| snapshot
2007-02-08	Claudio Sacerdoti...	More progress in technicalities/setoids.ma.	commit \| commitdiff \| tree \| snapshot
2007-02-08	Claudio Sacerdoti...	Manual for the "default" command updated.	commit \| commitdiff \| tree \| snapshot
2007-02-08	Claudio Sacerdoti...	* 'default "equality"' command changed to consider...	commit \| commitdiff \| tree \| snapshot
2007-02-08	Claudio Sacerdoti...	If a pretty printed term spans on multiple lines, then...	commit \| commitdiff \| tree \| snapshot
2007-02-08	Claudio Sacerdoti...	Important commit:	commit \| commitdiff \| tree \| snapshot
2007-02-08	Ferruccio Guidi	developments fixup	commit \| commitdiff \| tree \| snapshot
2007-02-08	Ferruccio Guidi	Unified refactored	commit \| commitdiff \| tree \| snapshot
2007-02-08	Ferruccio Guidi	definitions fixup	commit \| commitdiff \| tree \| snapshot
2007-02-08	Ferruccio Guidi	fix dependences for matita	commit \| commitdiff \| tree \| snapshot
2007-02-07	Ferruccio Guidi	LAMBDA-TYPES: refactored	commit \| commitdiff \| tree \| snapshot
2007-02-07	Ferruccio Guidi	refactoring	commit \| commitdiff \| tree \| snapshot
2007-02-07	Ferruccio Guidi	Level-1 refactored	commit \| commitdiff \| tree \| snapshot
2007-02-07	Ferruccio Guidi	refactoring	commit \| commitdiff \| tree \| snapshot
2007-02-07	Ferruccio Guidi	refactoring	commit \| commitdiff \| tree \| snapshot
2007-02-07	Claudio Sacerdoti...	New dependency over acic_procedural.	commit \| commitdiff \| tree \| snapshot
2007-02-06	Ferruccio Guidi	- Procedural: moved in a directory on its own	commit \| commitdiff \| tree \| snapshot
2007-02-06	Claudio Sacerdoti...	More stuff in technicalities/setoids.ma	commit \| commitdiff \| tree \| snapshot
2007-02-06	Claudio Sacerdoti...	Debugging deactivated.	commit \| commitdiff \| tree \| snapshot
2007-02-06	Claudio Sacerdoti...	Bug fixed in the computation of the disambiguation...	commit \| commitdiff \| tree \| snapshot
2007-02-06	Claudio Sacerdoti...	Incredible bug fixed in Fix and CoFix. The types of...	commit \| commitdiff \| tree \| snapshot
2007-02-05	Claudio Sacerdoti...	Second formulation of a constructive (positive) proof...	commit \| commitdiff \| tree \| snapshot
2007-02-02	Claudio Sacerdoti...	Serious bug fixed: the types of a real mutual fix defin...	commit \| commitdiff \| tree \| snapshot
2007-02-02	Ferruccio Guidi	added preamble file in LambdaDelta and improved theory...	commit \| commitdiff \| tree \| snapshot
2007-02-02	Ferruccio Guidi	The baseuris changed	commit \| commitdiff \| tree \| snapshot
2007-02-01	Ferruccio Guidi	Level-1: regenerated with differnt baseuris	commit \| commitdiff \| tree \| snapshot
2007-02-01	Enrico Tassi	restored coercions between eq and eq	commit \| commitdiff \| tree \| snapshot
2007-02-01	Enrico Tassi	reverted a commented substitution in build_newgoal...	commit \| commitdiff \| tree \| snapshot
2007-01-31	Ferruccio Guidi	methods eos, goto, advance and retract now catch Invali...	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom