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

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

2009-07-22	Claudio Sacerdoti...	Elimination principles are now processed in O(1) again	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	Major speed-up: meta-chains are now expanded during...	commit \| commitdiff \| tree \| snapshot
2009-07-22	denes	Fixed test for invertibility	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	1) PTS simplified	commit \| commitdiff \| tree \| snapshot
2009-07-22	denes	Now using lazy strings for debug printings	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	nelim fixed	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	leftno was List.length rights :-)	commit \| commitdiff \| tree \| snapshot
2009-07-22	Claudio Sacerdoti...	Almost ready to implement coercion declaration for...	commit \| commitdiff \| tree \| snapshot
2009-07-21	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-21	Claudio Sacerdoti...	1) record projections are now automatically generated	commit \| commitdiff \| tree \| snapshot
2009-07-21	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2009-07-21	Claudio Sacerdoti...	Record projections are now automatically generated...	commit \| commitdiff \| tree \| snapshot
2009-07-21	denes	Implemented handling of Invertible equalities	commit \| commitdiff \| tree \| snapshot
2009-07-20	Enrico Tassi	sorted modules	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	Debugging printf removed	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	nrewrite now uses the appropriate principle when going...	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	nrewrite now working	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-20	denes	Removed status printing by processes	commit \| commitdiff \| tree \| snapshot
2009-07-20	denes	Fixed multiple printing	commit \| commitdiff \| tree \| snapshot
2009-07-20	Wilmer Ricciotti	Final version, submitted to CASC-22.	commit \| commitdiff \| tree \| snapshot
2009-07-20	Wilmer Ricciotti	added a flag for age selection	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	Very serious bug fixed in unification, but the fix...	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	1) The NG kernel now accepts only usage of declared...	commit \| commitdiff \| tree \| snapshot
2009-07-20	denes	One-side indexing for commutativity	commit \| commitdiff \| tree \| snapshot
2009-07-20	denes	No demod call on functionnal symbols	commit \| commitdiff \| tree \| snapshot
2009-07-20	Claudio Sacerdoti...	1) ppmetasenv and ppcontext to reduce the amount of...	commit \| commitdiff \| tree \| snapshot
2009-07-19	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	nelim now uses the appropriate _rect_XXX elimination...	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	1) the user is notified when a new object is defined	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	More info to refine empty types elimination.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Old code commented out.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Generation of principles is now atomic.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Debugging code commented out.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Enrico Tassi	add comment	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Non reproducible.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Some bugs already fixed.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Bugs (mostly from Oliboni)	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Bug fixed: singleton application.	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	New suffixes for elimination principles:	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	1) added a function to retrieve all the universes curre...	commit \| commitdiff \| tree \| snapshot
2009-07-17	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-17	Claudio Sacerdoti...	Generation of inductive principle for Type[0].	commit \| commitdiff \| tree \| snapshot
2009-07-16	Cosimo Oliboni	freescale porting, work in progress	commit \| commitdiff \| tree \| snapshot
2009-07-16	denes	Sorted version of eligible problems list	commit \| commitdiff \| tree \| snapshot
2009-07-16	denes	Disabled age selection and ad hoc goal weight computation	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
next

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

RSS Atom