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

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

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
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
next

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

RSS Atom