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

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

2009-06-25	Enrico Tassi	initial import of standalone matitaprover binary	commit \| commitdiff \| tree
2009-06-25	Enrico Tassi	code refactoring for paramodulation	commit \| commitdiff \| tree
2009-06-25	Enrico Tassi	new function list_mapi_acc	commit \| commitdiff \| tree
2009-06-23	Enrico Tassi	undo/serialization for universes implemented	commit \| commitdiff \| tree
2009-06-23	Enrico Tassi	removed problem not in UEQ	commit \| commitdiff \| tree
2009-06-18	Enrico Tassi	debug pps removed	commit \| commitdiff \| tree
2009-06-18	Enrico Tassi	better exception handling	commit \| commitdiff \| tree
2009-06-18	Enrico Tassi	proof patching!	commit \| commitdiff \| tree
2009-06-18	Enrico Tassi	callbacks were taking in input a status bu were not...	commit \| commitdiff \| tree
2009-06-17	Enrico Tassi	proof reconstruction almost OK	commit \| commitdiff \| tree
2009-06-16	Enrico Tassi	first proof reconstruction attempt, still bugged since it	commit \| commitdiff \| tree
2009-06-16	Enrico Tassi	avoid fixing non-recursive terms	commit \| commitdiff \| tree
2009-06-16	Enrico Tassi	we fix recursive object reference with the correct...	commit \| commitdiff \| tree
2009-06-15	Enrico Tassi	EXPERIMENTAL COMMIT (part B, by CSC :-):	commit \| commitdiff \| tree
2009-06-15	Enrico Tassi	EXPERIMENTAL COMMIT (by CSC,actuall :-)	commit \| commitdiff \| tree
2009-06-15	Enrico Tassi	...	commit \| commitdiff \| tree
2009-06-15	Enrico Tassi	added TODO list	commit \| commitdiff \| tree
2009-06-15	Enrico Tassi	huge commit regarding the grafite_status:	commit \| commitdiff \| tree
2009-06-15	Enrico Tassi	part of last commit	commit \| commitdiff \| tree
2009-06-15	Enrico Tassi	tacticals are really tactics now, they have an AST...	commit \| commitdiff \| tree
2009-06-12	Enrico Tassi	-ng implemented	commit \| commitdiff \| tree
2009-06-11	Enrico Tassi	content2pres for the new cic fixed	commit \| commitdiff \| tree
2009-06-10	Enrico Tassi	1) added simplification of actives w.r.t. selected	commit \| commitdiff \| tree
2009-06-10	Enrico Tassi	right inference step completed	commit \| commitdiff \| tree
2009-06-10	Enrico Tassi	new function filter_map_acc	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	almost complete superposition right step	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	snapshot	commit \| commitdiff \| tree
2009-06-09	Enrico Tassi	see the previous commit	commit \| commitdiff \| tree
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
next

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

RSS Atom