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

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

2009-04-16	Enrico Tassi	Universe is used only locally to tactics/	commit \| commitdiff \| tree
2009-04-16	Enrico Tassi	added an exception	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	added letin, still broken	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	...	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	new tactic whd implemented	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	- change implemented in 4 lines	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	- generalize finished	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	?_OS1 := C[ ?_IN ]	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	fixed modules order	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	minor fixes	commit \| commitdiff \| tree
2009-04-09	Enrico Tassi	...	commit \| commitdiff \| tree
2009-04-08	Enrico Tassi	generalized is half-implemented (still broken)	commit \| commitdiff \| tree
2009-04-08	Enrico Tassi	Analizyng the inductive type of the eliminated term and	commit \| commitdiff \| tree
2009-04-07	Enrico Tassi	- select_tac honors the hypotheses pattern when required...	commit \| commitdiff \| tree
2009-04-07	Enrico Tassi	select honors the substitution	commit \| commitdiff \| tree
2009-04-06	Enrico Tassi	tactic cases works! delift clears tags	commit \| commitdiff \| tree
2009-04-06	Enrico Tassi	eta-contraction was made on the wrong term	commit \| commitdiff \| tree
2009-04-06	Enrico Tassi	unification:	commit \| commitdiff \| tree
2009-04-06	Enrico Tassi	better error message	commit \| commitdiff \| tree
2009-04-06	Enrico Tassi	added one exception	commit \| commitdiff \| tree
2009-04-06	Enrico Tassi	snapshot	commit \| commitdiff \| tree
2009-04-02	Enrico Tassi	...	commit \| commitdiff \| tree
2009-04-02	Enrico Tassi	New file nTacStatus to:	commit \| commitdiff \| tree
2009-04-02	Enrico Tassi	added analyse_indty	commit \| commitdiff \| tree
2009-04-01	Enrico Tassi	added tentative elim	commit \| commitdiff \| tree
2009-04-01	Enrico Tassi	1) mk_meta now returns also the index of the created...	commit \| commitdiff \| tree
2009-04-01	Enrico Tassi	removed spurious "	commit \| commitdiff \| tree
2009-03-30	Enrico Tassi	tentative subst-sexpand and change	commit \| commitdiff \| tree
2009-03-30	Enrico Tassi	...	commit \| commitdiff \| tree
2009-03-27	Enrico Tassi	more comments	commit \| commitdiff \| tree
2009-03-27	Enrico Tassi	exec and distribute implemented	commit \| commitdiff \| tree
2009-03-26	Enrico Tassi	new apply almost there	commit \| commitdiff \| tree
2009-03-26	Enrico Tassi	...	commit \| commitdiff \| tree
2009-03-26	Enrico Tassi	...	commit \| commitdiff \| tree
2009-03-25	Enrico Tassi	new tactics are almost ready	commit \| commitdiff \| tree
2009-03-16	Enrico Tassi	added mactions, the three can now be collapsed to fit...	commit \| commitdiff \| tree
2009-03-11	Enrico Tassi	unification hints with recursive calls do work!	commit \| commitdiff \| tree
2009-03-11	Enrico Tassi	added margin option to the pp	commit \| commitdiff \| tree
2009-03-11	Enrico Tassi	more examples	commit \| commitdiff \| tree
2009-03-10	Enrico Tassi	unificatiom hints with premises	commit \| commitdiff \| tree
2009-03-10	Enrico Tassi	unification hints almost ready	commit \| commitdiff \| tree
2009-03-10	Enrico Tassi	notation ++	commit \| commitdiff \| tree
2009-03-09	Enrico Tassi	...	commit \| commitdiff \| tree
2009-03-03	Enrico Tassi	- fixed hint generation, more hints are generated	commit \| commitdiff \| tree
2009-02-25	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-24	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-24	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-20	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-20	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-16	Enrico Tassi	some notational experiments	commit \| commitdiff \| tree
2009-02-15	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-15	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-15	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-15	Enrico Tassi	commented some printings	commit \| commitdiff \| tree
2009-02-15	Enrico Tassi	minor changes to make the library compile after wilmers...	commit \| commitdiff \| tree
2009-02-11	Enrico Tassi	some work to refine objs	commit \| commitdiff \| tree
2009-02-11	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-09	Enrico Tassi	b:action are now considered as m:maction and thus are...	commit \| commitdiff \| tree
2009-02-06	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-05	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-05	Enrico Tassi	a non necessary but morally required change. The matched...	commit \| commitdiff \| tree
2009-02-03	Enrico Tassi	some work to speed up the system	commit \| commitdiff \| tree
2009-02-03	Enrico Tassi	case tactic first tries with a simple outtype and then...	commit \| commitdiff \| tree
2009-02-02	Enrico Tassi	...	commit \| commitdiff \| tree
2009-02-02	Enrico Tassi	CicTypeChecker.typecheck now takes an additional parameter:	commit \| commitdiff \| tree
2009-01-30	Enrico Tassi	fix convertibility in case of application test_eq_only...	commit \| commitdiff \| tree
2009-01-29	Enrico Tassi	more polishing	commit \| commitdiff \| tree
2009-01-29	Enrico Tassi	...	commit \| commitdiff \| tree
2009-01-29	Enrico Tassi	application arguments are compared with test_eq_only...	commit \| commitdiff \| tree
2009-01-28	Enrico Tassi	some work	commit \| commitdiff \| tree
2009-01-28	Enrico Tassi	...	commit \| commitdiff \| tree
2009-01-28	Enrico Tassi	...	commit \| commitdiff \| tree
2009-01-28	Enrico Tassi	...	commit \| commitdiff \| tree
2009-01-28	Enrico Tassi	...	commit \| commitdiff \| tree
2009-01-27	Enrico Tassi	maction, mpadded and mstyle added to documentation	commit \| commitdiff \| tree
2009-01-26	Enrico Tassi	minor fixes	commit \| commitdiff \| tree
2009-01-26	Enrico Tassi	maction support added to notation, adopted for = AKA...	commit \| commitdiff \| tree
2009-01-26	Enrico Tassi	maction layout added to notation	commit \| commitdiff \| tree
2009-01-26	Enrico Tassi	we were generating a name for the main fix twice	commit \| commitdiff \| tree
2009-01-26	Enrico Tassi	added a number to identical error messages to ease...	commit \| commitdiff \| tree
2009-01-21	Enrico Tassi	some minor fixes	commit \| commitdiff \| tree
2009-01-21	Enrico Tassi	a bit of work done while travelling to padova	commit \| commitdiff \| tree
2009-01-19	Enrico Tassi	- new notation.ma file with local and common notation	commit \| commitdiff \| tree
2009-01-19	Enrico Tassi	all pullbacks are attempted in sequence, removed many...	commit \| commitdiff \| tree
2009-01-16	Enrico Tassi	ceommented out metasenv	commit \| commitdiff \| tree
2009-01-16	Enrico Tassi	...	commit \| commitdiff \| tree
2009-01-15	Enrico Tassi	the new coercion behaviour (variants + composition...	commit \| commitdiff \| tree
2009-01-15	Enrico Tassi	added notation for 'Vdash	commit \| commitdiff \| tree
2009-01-15	Enrico Tassi	if the user attempts to insert a duplicate coercions...	commit \| commitdiff \| tree
2009-01-15	Enrico Tassi	unvariant also for coercions to funclass	commit \| commitdiff \| tree
2009-01-15	Enrico Tassi	- name mangling changed, added __ to separate additional...	commit \| commitdiff \| tree
2009-01-15	Enrico Tassi	no more universe inconsistency printed to stderr	commit \| commitdiff \| tree
2009-01-15	Enrico Tassi	coercions that are marked as variant are unfolded when...	commit \| commitdiff \| tree
2009-01-15	Enrico Tassi	Coercions graph is printed between real types and not...	commit \| commitdiff \| tree
2009-01-13	Enrico Tassi	many changes regarding coercions:	commit \| commitdiff \| tree
2009-01-08	Enrico Tassi	more composites to make all happy!	commit \| commitdiff \| tree
2009-01-08	Enrico Tassi	eq over SET1 and SET no longer used	commit \| commitdiff \| tree
2009-01-08	Enrico Tassi	some more if/fi conversion due to the new . binding	commit \| commitdiff \| tree
2009-01-08	Enrico Tassi	unary_morphism_N : seoidN -> setoidN -> setoidN (was...	commit \| commitdiff \| tree
2009-01-08	Enrico Tassi	virtuals for () removed and bound to 'o'	commit \| commitdiff \| tree
next

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

RSS Atom