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

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

2009-06-09	Enrico Tassi	termAcicContent is logic independent (despite its name...	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	snaphost: supright almost done	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	fixed metas	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	fixed building	commit \| commitdiff \| tree
2009-06-08	Enrico Tassi	...	commit \| commitdiff \| tree
2009-06-08	Enrico Tassi	a skeleton of supright	commit \| commitdiff \| tree
2009-06-08	Enrico Tassi	some more functors and a nice higher-order all_positions...	commit \| commitdiff \| tree
2009-06-08	Enrico Tassi	added META for ng_paramodulation	commit \| commitdiff \| tree
2009-06-06	Enrico Tassi	some renaming to make ocamlopt happy	commit \| commitdiff \| tree
2009-06-04	Enrico Tassi	minor changes here and there. We extend fo-unification...	commit \| commitdiff \| tree
2009-06-04	Enrico Tassi	comments	commit \| commitdiff \| tree
2009-06-04	Enrico Tassi	better type for comparison and implementation of KBO...	commit \| commitdiff \| tree
2009-06-04	Enrico Tassi	more functors	commit \| commitdiff \| tree
2009-06-03	Enrico Tassi	functorial abstraction over term blobs	commit \| commitdiff \| tree
2009-06-01	Enrico Tassi	added a snapshot of comparison	commit \| commitdiff \| tree
2009-06-01	Enrico Tassi	we rewrite the paramodulation code!	commit \| commitdiff \| tree
2009-05-25	Enrico Tassi	nasty change in the lexer/parser:	commit \| commitdiff \| tree
2009-05-19	Enrico Tassi	...	commit \| commitdiff \| tree
2009-05-19	Enrico Tassi	regenerated	commit \| commitdiff \| tree
2009-05-19	Enrico Tassi	fixed generation of horn clauses, negated atoms are...	commit \| commitdiff \| tree
2009-05-19	Enrico Tassi	some horn+equality problems	commit \| commitdiff \| tree
2009-05-18	Enrico Tassi	removed useless function	commit \| commitdiff \| tree
2009-05-18	Enrico Tassi	in the new kernel you can type Type[i] to mean Type_i...	commit \| commitdiff \| tree
2009-05-18	Enrico Tassi	nothing special	commit \| commitdiff \| tree
2009-05-17	Enrico Tassi	byte tests disabled	commit \| commitdiff \| tree
2009-05-15	Enrico Tassi	added patch to not unify any term containing the in_scope...	commit \| commitdiff \| tree
2009-05-06	Enrico Tassi	apply and auto.equational_case call saturation.solve_narrowing	commit \| commitdiff \| tree
2009-05-06	Enrico Tassi	updated comment	commit \| commitdiff \| tree
2009-05-05	Enrico Tassi	- pretty printer made robust in face of list_nth	commit \| commitdiff \| tree
2009-05-05	Enrico Tassi	more tests	commit \| commitdiff \| tree
2009-04-30	Enrico Tassi	run check_if_goal_is_solved on all goals (active+passive)	commit \| commitdiff \| tree
2009-04-29	Enrico Tassi	...	commit \| commitdiff \| tree
2009-04-29	Enrico Tassi	call paramod instead of solve_Rewrite	commit \| commitdiff \| tree
2009-04-29	Enrico Tassi	no typing	commit \| commitdiff \| tree
2009-04-29	Enrico Tassi	many checks guarded with if Utils.debug_metas	commit \| commitdiff \| tree
2009-04-28	Enrico Tassi	depenalization of smart apply inside auto, that is...	commit \| commitdiff \| tree
2009-04-28	Enrico Tassi	fixed bug, demodulation was keeping results not strictly...	commit \| commitdiff \| tree
2009-04-28	Enrico Tassi	huge commit in automation:	commit \| commitdiff \| tree
2009-04-22	Enrico Tassi	demodulate takes an extra argument 'all', if present...	commit \| commitdiff \| tree
2009-04-21	Enrico Tassi	fixed last file restricting auto tables	commit \| commitdiff \| tree
2009-04-20	Enrico Tassi	- init_cache_and_tables rewritten using the automation_cache	commit \| commitdiff \| tree
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
next

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

RSS Atom