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

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

2007-11-15	Enrico Tassi	tagging rc-1 0.4.95 0.4.95	commit \| commitdiff \| tree \| snapshot
2007-11-15	Enrico Tassi	rc-1 0.4.95@7852 0.4.95@7852	commit \| commitdiff \| tree \| snapshot
2007-11-15	Enrico Tassi	added ~delta parameter to saturate_term and used it...	commit \| commitdiff \| tree \| snapshot
2007-11-14	Claudio Sacerdoti...	Bug fixed: yet another case where tys of mutual recursi...	commit \| commitdiff \| tree \| snapshot
2007-11-14	Enrico Tassi	xxx	commit \| commitdiff \| tree \| snapshot
2007-11-14	Ferruccio Guidi	now destruct takes an optional list of term rather...	commit \| commitdiff \| tree \| snapshot
2007-11-14	Enrico Tassi	fixed notation	commit \| commitdiff \| tree \| snapshot
2007-11-14	Enrico Tassi	ogroups almost finished	commit \| commitdiff \| tree \| snapshot
2007-11-14	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2007-11-14	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2007-11-13	Enrico Tassi	End of groups :-)	commit \| commitdiff \| tree \| snapshot
2007-11-13	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2007-11-13	Ferruccio Guidi	- ProofEngineHelpers: namer_of moved to GrafiteEngine	commit \| commitdiff \| tree \| snapshot
2007-11-13	Ferruccio Guidi	previously hidden simplifications (in old destruct...	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	some work till the need of redoing all groups based...	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	since there is no more tab, the modification of the...	commit \| commitdiff \| tree \| snapshot
2007-11-12	Ferruccio Guidi	- destruct tactic: automatic simplification in case...	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	removed ugly printing	commit \| commitdiff \| tree \| snapshot
2007-11-12	Enrico Tassi	ordered_sets are built with excedence	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom