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

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

2007-11-12	Enrico Tassi	added ordered sets	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	renamed ordered sets into excedence.ma	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	relocated	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	removed dust	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	HIDDEN (since glade do not read out file properly anymo...	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	new file with some relations stated in Type	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	ordered set is over, much new stuff coming from a coref...	commit \| commitdiff \| tree \| snapshot
2007-11-12	Ferruccio Guidi	refactoring	commit \| commitdiff \| tree \| snapshot
2007-11-10	Ferruccio Guidi	old subst tactics removed. New destruct tactic used...	commit \| commitdiff \| tree \| snapshot
2007-11-10	Claudio Sacerdoti...	a) Detection of existential types now implemented	commit \| commitdiff \| tree \| snapshot
2007-11-10	Claudio Sacerdoti...	More correct (but still bugged) implementation of type...	commit \| commitdiff \| tree \| snapshot
2007-11-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree \| snapshot
2007-11-09	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2007-11-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2007-11-08	Ferruccio Guidi	- subst tactic keyword removed from highlight syntax...	commit \| commitdiff \| tree \| snapshot
2007-11-08	Claudio Sacerdoti...	Trivial bug fixed in type inference of LetIn source...	commit \| commitdiff \| tree \| snapshot
2007-11-08	Enrico Tassi	xxx	commit \| commitdiff \| tree \| snapshot
2007-11-08	Enrico Tassi	ported to the new destruct	commit \| commitdiff \| tree \| snapshot
2007-11-08	Claudio Sacerdoti...	Arguments of constructors in a case pattern are now...	commit \| commitdiff \| tree \| snapshot
2007-11-08	Claudio Sacerdoti...	svn:ignore set	commit \| commitdiff \| tree \| snapshot
2007-11-08	Enrico Tassi	please, commit files with debug=false otherwise the...	commit \| commitdiff \| tree \| snapshot
2007-11-08	Enrico Tassi	forced associativity in if construct	commit \| commitdiff \| tree \| snapshot
2007-11-08	Claudio Sacerdoti...	Zoli's note (in Italian) about a constructive version...	commit \| commitdiff \| tree \| snapshot
2007-11-07	Ferruccio Guidi	set svn:ignore to *.ml in the deve directories	commit \| commitdiff \| tree \| snapshot
2007-11-07	Ferruccio Guidi	- bug fix in destruct	commit \| commitdiff \| tree \| snapshot
2007-11-07	Enrico Tassi	reorganization of the whole story, the root dir contain...	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom