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

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

2007-11-07	Enrico Tassi	Code extraction unbranched again.	commit \| commitdiff \| tree \| snapshot
2007-11-06	Ferruccio Guidi	new implementation of the destruct tactic,	commit \| commitdiff \| tree \| snapshot
2007-11-06	Claudio Sacerdoti...	cic_acic should be compiled before cic_exportation	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	Bug in detection of too polymorphic types partially...	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	MutCases that occur in types should be handled with...	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	Obj.magic are now generated to extract dependently...	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	Handling of left parameters of constructors/indutive...	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	Slightly nicer output.	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	Filenames are now fully mangled (e.g. matita_nat_nat...	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	Type application and abstractions are now exported...	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	New OCaml keyword "val".	commit \| commitdiff \| tree \| snapshot
2007-11-05	Claudio Sacerdoti...	"f" => "aux" to avoid name clashes	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	The type parameters in an inductive type declaration...	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	Type arguments are better uncapitalized.	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	Empty types not in Prop and empty types elimination...	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	Empty and singleton type elimination are now handled...	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	1. type definitions of propositions are no longer expor...	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	Bug fixed: qualified names were not generated correctly...	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	* type definitions that define a new proposition are...	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	CicExportation branched. Change "if false" with "if...	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	All exported names are now qualified. This avoids the...	commit \| commitdiff \| tree \| snapshot
2007-11-04	Claudio Sacerdoti...	All names are now qualified. This avoids the need for...	commit \| commitdiff \| tree \| snapshot
2007-11-02	Claudio Sacerdoti...	* Very experimental and not branched *	commit \| commitdiff \| tree \| snapshot
2007-11-02	Ferruccio Guidi	- tacticals: new tactical ifs added: uses thens where...	commit \| commitdiff \| tree \| snapshot
2007-11-02	Claudio Sacerdoti...	Added an hook useful in many situations.	commit \| commitdiff \| tree \| snapshot
2007-11-02	Enrico Tassi	finisced configuration section	commit \| commitdiff \| tree \| snapshot
2007-11-02	Enrico Tassi	added doc for db and getter sections	commit \| commitdiff \| tree \| snapshot
2007-11-02	Enrico Tassi	added notes about sqlite and removed obsolete zack...	commit \| commitdiff \| tree \| snapshot
2007-10-31	Claudio Sacerdoti...	New image from Tassi's PhD thesis.	commit \| commitdiff \| tree \| snapshot
2007-10-30	Ferruccio Guidi	better implementation of if_	commit \| commitdiff \| tree \| snapshot
2007-10-30	Enrico Tassi	remade dependencies that were wrong	commit \| commitdiff \| tree \| snapshot
2007-10-29	Ferruccio Guidi	- destruct: core of subst tactic implemented,	commit \| commitdiff \| tree \| snapshot
2007-10-29	Ferruccio Guidi	reverted matita db configuration fixed	commit \| commitdiff \| tree \| snapshot
2007-10-28	Claudio Sacerdoti...	Bug fixed: patterns in hypotheses under binders where...	commit \| commitdiff \| tree \| snapshot
2007-10-28	Claudio Sacerdoti...	New syntax for match patterns in terms and in patterns.	commit \| commitdiff \| tree \| snapshot
2007-10-28	Claudio Sacerdoti...	The document was not valid. Fixed.	commit \| commitdiff \| tree \| snapshot
2007-10-28	Claudio Sacerdoti...	Pretty-printing of "match ... with" pattern syntax...	commit \| commitdiff \| tree \| snapshot
2007-10-28	Claudio Sacerdoti...	Nil => nil, Cons => cons	commit \| commitdiff \| tree \| snapshot
2007-10-28	Claudio Sacerdoti...	Nil => nil; Cons => cons	commit \| commitdiff \| tree \| snapshot
2007-10-28	Claudio Sacerdoti...	New syntax for match patterns.	commit \| commitdiff \| tree \| snapshot
2007-10-28	Enrico Tassi	clean can't fail	commit \| commitdiff \| tree \| snapshot
2007-10-28	Enrico Tassi	added patch for the configuration file	commit \| commitdiff \| tree \| snapshot
2007-10-28	Enrico Tassi	reverted last commit	commit \| commitdiff \| tree \| snapshot
2007-10-26	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2007-10-26	Enrico Tassi	rebuilt	commit \| commitdiff \| tree \| snapshot
2007-10-26	Enrico Tassi	no -rectype passed to ocamldep	commit \| commitdiff \| tree \| snapshot
2007-10-26	Enrico Tassi	rebuilt	commit \| commitdiff \| tree \| snapshot
2007-10-26	Enrico Tassi	0.4.0 almost working	commit \| commitdiff \| tree \| snapshot
2007-10-26	Claudio Sacerdoti...	Syntax of patterns changed (and not documented yet).	commit \| commitdiff \| tree \| snapshot
2007-10-26	Claudio Sacerdoti...	Wildcard patterns implemented in case analysis. The...	commit \| commitdiff \| tree \| snapshot
2007-10-26	Enrico Tassi	we use ulex08 not ulex	commit \| commitdiff \| tree \| snapshot
2007-10-25	Ferruccio Guidi	bug fix in injection e relocate term	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	neg => Qneg :-)	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	true and false were swapped!	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	flase => false :-)	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	Ooops. In previous commit I forgot to subtract the...	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	Bug fixed: case analysis where a case had not the expec...	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	Bug fixed: a MutCase considering a wrong number of...	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	Bug fixed: a MutCase with missing or exceeding cases...	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	1. More localization: interpretation errors are now...	commit \| commitdiff \| tree \| snapshot
2007-10-25	Claudio Sacerdoti...	Recently introduced bug fixed: error localization was...	commit \| commitdiff \| tree \| snapshot
2007-10-24	Ferruccio Guidi	bug fix in injection: we have to recur on the generated...	commit \| commitdiff \| tree \| snapshot
2007-10-24	Ferruccio Guidi	we revisited the implementation of the destruct tactic...	commit \| commitdiff \| tree \| snapshot
2007-10-24	Claudio Sacerdoti...	Debugging code improved.	commit \| commitdiff \| tree \| snapshot
2007-10-24	Ferruccio Guidi	- new function for general relocation of local referenc...	commit \| commitdiff \| tree \| snapshot
2007-10-22	Enrico Tassi	fixed copyright file... an ITP should be done	commit \| commitdiff \| tree \| snapshot
2007-10-16	Claudio Sacerdoti...	Interesting. Do we need many more inversion lemmas...	commit \| commitdiff \| tree \| snapshot
2007-10-16	Enrico Tassi	fixed make opt	commit \| commitdiff \| tree \| snapshot
2007-10-16	Claudio Sacerdoti...	DOS-style CR+LF added to the blanks list.	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	Dead code clean-up.	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	The behaviour of autobatch paramodulation has changed.	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	Wrong test patched.	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	discriminate.ma => destruct.ma	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	Spurious code removed.	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	Old wrong code to avoid old bug fixed.	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	Stupid bug fixed.	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	auto ==> autobatch	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	Stupid bug fixed (I deleted "assumption a" by error).	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	auto => autobatch	commit \| commitdiff \| tree \| snapshot
2007-10-15	Claudio Sacerdoti...	auto => autobatch	commit \| commitdiff \| tree \| snapshot
2007-10-14	Claudio Sacerdoti...	Caseness problems fixed.	commit \| commitdiff \| tree \| snapshot
2007-10-14	Claudio Sacerdoti...	Some lemmas moves to the file they belong to.	commit \| commitdiff \| tree \| snapshot
2007-10-14	Cristian Armentano	Theorem sigma_p_knm changed into generic_iter_p_knm.	commit \| commitdiff \| tree \| snapshot
2007-10-13	Ferruccio Guidi	- some new auxiliary lemmas	commit \| commitdiff \| tree \| snapshot
2007-10-13	Ferruccio Guidi	removed unused notation =>	commit \| commitdiff \| tree \| snapshot
2007-10-12	Claudio Sacerdoti...	Move to OCaml 3.10. Requires debian packages from unsta...	commit \| commitdiff \| tree \| snapshot
2007-10-12	Wilmer Ricciotti	Fixed baseuri	commit \| commitdiff \| tree \| snapshot
2007-10-12	Wilmer Ricciotti	Part1a update...	commit \| commitdiff \| tree \| snapshot
2007-10-12	Andrea Asperti	More restructuring in moebius.ma	commit \| commitdiff \| tree \| snapshot
2007-10-12	Andrea Asperti	Reorganization of the library.	commit \| commitdiff \| tree \| snapshot
2007-10-12	Andrea Asperti	Reorganization of the library.	commit \| commitdiff \| tree \| snapshot
2007-10-12	Andrea Asperti	Reorganization of results.	commit \| commitdiff \| tree \| snapshot
2007-10-11	Claudio Sacerdoti...	Old inversion bug fixed: it used to work only on the...	commit \| commitdiff \| tree \| snapshot
2007-10-09	Enrico Tassi	added patch to allow i,j,k: skip and *: skip	commit \| commitdiff \| tree \| snapshot
2007-10-08	Andrea Asperti	Some axioms for Q.	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom