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

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

2009-09-25	denes	Ported innermost strategy for demodulation from trunk	commit \| commitdiff \| tree \| snapshot
2009-07-31	denes	Fixed (yet another) nasty bug, in deep_eq this time	commit \| commitdiff \| tree \| snapshot
2009-07-31	denes	Fixed nasty bug in superposition and freshing of clauses	commit \| commitdiff \| tree \| snapshot
2009-07-31	denes	Now iterating superposition	commit \| commitdiff \| tree \| snapshot
2009-07-30	denes	Ported demodulation on clauses	commit \| commitdiff \| tree \| snapshot
2009-07-30	denes	Added check for trivial (identity) goal	commit \| commitdiff \| tree \| snapshot
2009-07-29	denes	Update eligible problem list (now sorted)	commit \| commitdiff \| tree \| snapshot
2009-07-29	denes	Added TreeLimitRun	commit \| commitdiff \| tree \| snapshot
2009-07-29	denes	Added Clauses module	commit \| commitdiff \| tree \| snapshot
2009-07-29	denes	Added symbolic link to clauses	commit \| commitdiff \| tree \| snapshot
2009-07-29	denes	Reorganized foUtils, added Clauses module to avoid...	commit \| commitdiff \| tree \| snapshot
2009-07-28	denes	Various architectural changes	commit \| commitdiff \| tree \| snapshot
2009-07-28	denes	Various architectural changes	commit \| commitdiff \| tree \| snapshot
2009-07-24	denes	Added symbolic links to hTopoSort	commit \| commitdiff \| tree \| snapshot
2009-07-24	denes	Fixed pretty printer and debug printings	commit \| commitdiff \| tree \| snapshot
2009-07-23	denes	First compiling version	commit \| commitdiff \| tree \| snapshot
2009-07-23	denes	Fixed useage	commit \| commitdiff \| tree \| snapshot
2009-07-22	denes	Fixes	commit \| commitdiff \| tree \| snapshot
2009-07-22	denes	Fixed conflicts due to problem when merging with UEQ...	commit \| commitdiff \| tree \| snapshot
2009-07-17	denes	Branched paramodulation for CNF (Horn clauses)	commit \| commitdiff \| tree \| snapshot
2009-07-15	Enrico Tassi	ncopy partially implemented and fixed (a ?) chain to...	commit \| commitdiff \| tree \| snapshot
2009-07-15	Wilmer Ricciotti	Fixed dependency function, which was lacking the code...	commit \| commitdiff \| tree \| snapshot
2009-07-15	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-07-15	Enrico Tassi	match_coercion gives back the saturations, not the...	commit \| commitdiff \| tree \| snapshot
2009-07-15	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-14	denes	Fixed Option type error (OCaml bug)	commit \| commitdiff \| tree \| snapshot
2009-07-14	denes	.	commit \| commitdiff \| tree \| snapshot
2009-07-14	denes	.	commit \| commitdiff \| tree \| snapshot
2009-07-14	Cosimo Oliboni	freescale porting to ng, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-13	Enrico Tassi	better spacing	commit \| commitdiff \| tree \| snapshot
2009-07-13	Enrico Tassi	statistics are used, when possible, to sort	commit \| commitdiff \| tree \| snapshot
2009-07-13	denes	Added statistics printings	commit \| commitdiff \| tree \| snapshot
2009-07-13	denes	Added statistics module	commit \| commitdiff \| tree \| snapshot
2009-07-13	Claudio Sacerdoti...	First proof finished (some tactics still not working).	commit \| commitdiff \| tree \| snapshot
2009-07-13	Enrico Tassi	matitaprover is now flexible enough to allow the comput...	commit \| commitdiff \| tree \| snapshot
2009-07-13	Claudio Sacerdoti...	Coercion hiding implemented. Notes:	commit \| commitdiff \| tree \| snapshot
2009-07-13	Cosimo Oliboni	freescale translation (work in progress)	commit \| commitdiff \| tree \| snapshot
2009-07-12	Cosimo Oliboni	(no commit message)	commit \| commitdiff \| tree \| snapshot
2009-07-11	Cosimo Oliboni	(no commit message)	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	Composite coercions are here!	commit \| commitdiff \| tree \| snapshot
2009-07-10	Ferruccio Guidi	- brgOutput: the nodes count is now implemented	commit \| commitdiff \| tree \| snapshot
2009-07-10	Enrico Tassi	initial implementation of coercion composition	commit \| commitdiff \| tree \| snapshot
2009-07-10	Enrico Tassi	more work on coercions composition	commit \| commitdiff \| tree \| snapshot
2009-07-10	Cosimo Oliboni	+root +depends	commit \| commitdiff \| tree \| snapshot
2009-07-10	denes	Removed unused parameter of unification procedure ...	commit \| commitdiff \| tree \| snapshot
2009-07-10	Enrico Tassi	more profilers	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	Coercions used here and there.	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	Bug fixed (missing ctx) + comment added.	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-10	Cosimo Oliboni	new ng freescale, no external dependencies	commit \| commitdiff \| tree \| snapshot
2009-07-10	Claudio Sacerdoti...	Let's live with new ocaml type system limitations...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	initial implementation of `ncoercion name : type :...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	claudio, please have a look at this	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	new nrepeat (and block '('...')' ) tactical	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	New functorialization: paramod is abstracted over a...	commit \| commitdiff \| tree \| snapshot
2009-07-09	denes	Fixed check for condition iv p.33 (Riazzanov)	commit \| commitdiff \| tree \| snapshot
2009-07-09	Wilmer Ricciotti	More updates to Fsub.	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	profile most operations, do not return a filtered varli...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	1 process for now	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	two cases should be assert false at least in TPTP	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	micro optimizations to unification	commit \| commitdiff \| tree \| snapshot
2009-07-09	denes	Cleaned a bit	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Enrico Tassi	activate kbo, not lpo	commit \| commitdiff \| tree \| snapshot
2009-07-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-09	Claudio Sacerdoti...	Bug fixed (non-captured variable).	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	eq moved to CProp	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	repeat_tac	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Enrico Tassi	few more files, one diverges	commit \| commitdiff \| tree \| snapshot
2009-07-08	Cosimo Oliboni	directory for porting the assembly to matita-ng	commit \| commitdiff \| tree \| snapshot
2009-07-08	Enrico Tassi	removed useless universes	commit \| commitdiff \| tree \| snapshot
2009-07-08	Enrico Tassi	import of a sample for cosimo	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Hmmmm. This way we need "canonical structures" also...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Metavariable case in does_not_occur (hence weakly/stric...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Missing case for Match implemented.	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	weakly/strictly positive checks relaxed to allow metava...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Improved error message.	commit \| commitdiff \| tree \| snapshot
2009-07-08	Claudio Sacerdoti...	Bug fixed: the debrujinate function (hence the one...	commit \| commitdiff \| tree \| snapshot
2009-07-07	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-07	Claudio Sacerdoti...	Bug fixed: one uri was not refreshed, causing divergenc...	commit \| commitdiff \| tree \| snapshot
2009-07-07	Enrico Tassi	fixed some typos	commit \| commitdiff \| tree \| snapshot
2009-07-07	Claudio Sacerdoti...	Let's play a bit with NG.	commit \| commitdiff \| tree \| snapshot
2009-07-07	Claudio Sacerdoti...	1) Include files for NG were neither recursively proces...	commit \| commitdiff \| tree \| snapshot
2009-07-06	denes	Fixed printing of number of problems solved	commit \| commitdiff \| tree \| snapshot
2009-07-06	denes	Tried to implement lpo in a more efficient way	commit \| commitdiff \| tree \| snapshot
2009-07-06	denes	Fixed typo in lpo (from old implementation)	commit \| commitdiff \| tree \| snapshot
2009-07-03	Ferruccio Guidi	some corrections	commit \| commitdiff \| tree \| snapshot
2009-07-03	Ferruccio Guidi	more static analysis on the Automath text	commit \| commitdiff \| tree \| snapshot
2009-07-03	denes	Ported old implementation of LPO (for test purposes)	commit \| commitdiff \| tree \| snapshot
2009-07-03	Ferruccio Guidi	we now do some static analysis on the Automath text...	commit \| commitdiff \| tree \| snapshot
2009-07-03	denes	Implemented LPO	commit \| commitdiff \| tree \| snapshot
2009-07-02	denes	Corrected type for bag	commit \| commitdiff \| tree \| snapshot
2009-07-02	denes	New age selection	commit \| commitdiff \| tree \| snapshot
2009-07-02	Enrico Tassi	better output handling	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom