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

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components

[helm.git] / helm / software / components /

2009-07-22	Claudio Sacerdoti...	Almost ready to implement coercion declaration for...	tree \| commitdiff
2009-07-21	Claudio Sacerdoti...	Debugging code removed.	tree \| commitdiff
2009-07-21	Claudio Sacerdoti...	Record projections are now automatically generated...	tree \| commitdiff
2009-07-21	denes	Implemented handling of Invertible equalities	tree \| commitdiff
2009-07-20	Enrico Tassi	sorted modules	tree \| commitdiff
2009-07-20	Claudio Sacerdoti...	Debugging printf removed	tree \| commitdiff
2009-07-20	Claudio Sacerdoti...	nrewrite now uses the appropriate principle when going...	tree \| commitdiff
2009-07-20	denes	Removed status printing by processes	tree \| commitdiff
2009-07-20	denes	Fixed multiple printing	tree \| commitdiff
2009-07-20	Wilmer Ricciotti	Final version, submitted to CASC-22.	tree \| commitdiff
2009-07-20	Wilmer Ricciotti	added a flag for age selection	tree \| commitdiff
2009-07-20	Claudio Sacerdoti...	Very serious bug fixed in unification, but the fix...	tree \| commitdiff
2009-07-20	Claudio Sacerdoti...	1) The NG kernel now accepts only usage of declared...	tree \| commitdiff
2009-07-20	denes	One-side indexing for commutativity	tree \| commitdiff
2009-07-20	denes	No demod call on functionnal symbols	tree \| commitdiff
2009-07-20	Claudio Sacerdoti...	1) ppmetasenv and ppcontext to reduce the amount of...	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	nelim now uses the appropriate _rect_XXX elimination...	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	1) the user is notified when a new object is defined	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	More info to refine empty types elimination.	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	Generation of principles is now atomic.	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	Debugging code commented out.	tree \| commitdiff
2009-07-17	Enrico Tassi	add comment	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	Bug fixed: singleton application.	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	New suffixes for elimination principles:	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	1) added a function to retrieve all the universes curre...	tree \| commitdiff
2009-07-17	Claudio Sacerdoti...	Generation of inductive principle for Type[0].	tree \| commitdiff
2009-07-16	denes	Sorted version of eligible problems list	tree \| commitdiff
2009-07-16	denes	Disabled age selection and ad hoc goal weight computation	tree \| commitdiff
2009-07-15	Enrico Tassi	ncopy partially implemented and fixed (a ?) chain to...	tree \| commitdiff
2009-07-15	Wilmer Ricciotti	Fixed dependency function, which was lacking the code...	tree \| commitdiff
2009-07-15	Enrico Tassi	...	tree \| commitdiff
2009-07-15	Enrico Tassi	match_coercion gives back the saturations, not the...	tree \| commitdiff
2009-07-14	denes	Fixed Option type error (OCaml bug)	tree \| commitdiff
2009-07-14	denes	.	tree \| commitdiff
2009-07-14	denes	.	tree \| commitdiff
2009-07-13	Enrico Tassi	better spacing	tree \| commitdiff
2009-07-13	Enrico Tassi	statistics are used, when possible, to sort	tree \| commitdiff
2009-07-13	denes	Added statistics printings	tree \| commitdiff
2009-07-13	denes	Added statistics module	tree \| commitdiff
2009-07-13	Enrico Tassi	matitaprover is now flexible enough to allow the comput...	tree \| commitdiff
2009-07-13	Claudio Sacerdoti...	Coercion hiding implemented. Notes:	tree \| commitdiff
2009-07-10	Enrico Tassi	initial implementation of coercion composition	tree \| commitdiff
2009-07-10	denes	Removed unused parameter of unification procedure ...	tree \| commitdiff
2009-07-10	Enrico Tassi	more profilers	tree \| commitdiff
2009-07-10	Claudio Sacerdoti...	Bug fixed (missing ctx) + comment added.	tree \| commitdiff
2009-07-09	Enrico Tassi	initial implementation of `ncoercion name : type :...	tree \| commitdiff
2009-07-09	Enrico Tassi	new nrepeat (and block '('...')' ) tactical	tree \| commitdiff
2009-07-09	Enrico Tassi	New functorialization: paramod is abstracted over a...	tree \| commitdiff
2009-07-09	denes	Fixed check for condition iv p.33 (Riazzanov)	tree \| commitdiff
2009-07-09	Enrico Tassi	profile most operations, do not return a filtered varli...	tree \| commitdiff
2009-07-09	Enrico Tassi	1 process for now	tree \| commitdiff
2009-07-09	Enrico Tassi	two cases should be assert false at least in TPTP	tree \| commitdiff
2009-07-09	Enrico Tassi	micro optimizations to unification	tree \| commitdiff
2009-07-09	denes	Cleaned a bit	tree \| commitdiff
2009-07-09	Enrico Tassi	...	tree \| commitdiff
2009-07-09	Enrico Tassi	activate kbo, not lpo	tree \| commitdiff
2009-07-09	Claudio Sacerdoti...	Bug fixed (non-captured variable).	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	repeat_tac	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	Metavariable case in does_not_occur (hence weakly/stric...	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	Missing case for Match implemented.	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	weakly/strictly positive checks relaxed to allow metava...	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	Improved error message.	tree \| commitdiff
2009-07-08	Claudio Sacerdoti...	Bug fixed: the debrujinate function (hence the one...	tree \| commitdiff
2009-07-07	Claudio Sacerdoti...	Bug fixed: one uri was not refreshed, causing divergenc...	tree \| commitdiff
2009-07-07	Claudio Sacerdoti...	1) Include files for NG were neither recursively proces...	tree \| commitdiff
2009-07-06	denes	Fixed printing of number of problems solved	tree \| commitdiff
2009-07-06	denes	Tried to implement lpo in a more efficient way	tree \| commitdiff
2009-07-06	denes	Fixed typo in lpo (from old implementation)	tree \| commitdiff
2009-07-03	denes	Ported old implementation of LPO (for test purposes)	tree \| commitdiff
2009-07-03	denes	Implemented LPO	tree \| commitdiff
2009-07-02	denes	Corrected type for bag	tree \| commitdiff
2009-07-02	denes	New age selection	tree \| commitdiff
2009-07-02	Enrico Tassi	better output handling	tree \| commitdiff
2009-07-02	Enrico Tassi	return type of paramod fixed according to the SZSOntology	tree \| commitdiff
2009-07-01	Enrico Tassi	...	tree \| commitdiff
2009-07-01	Enrico Tassi	...	tree \| commitdiff
2009-07-01	Wilmer Ricciotti	Version number set to 1.0.0-rc1	tree \| commitdiff
2009-07-01	denes	Fixed type of bag	tree \| commitdiff
2009-06-30	Enrico Tassi	parallel	tree \| commitdiff
2009-06-30	denes	Moved ID management inside the bag	tree \| commitdiff
2009-06-30	Enrico Tassi	attempt of using 2 different orderings	tree \| commitdiff
2009-06-30	Enrico Tassi	....	tree \| commitdiff
2009-06-30	denes	Corrected a few typos	tree \| commitdiff
2009-06-30	Enrico Tassi	...	tree \| commitdiff
2009-06-30	denes	Enabled age selection (ratio 1/5)	tree \| commitdiff
2009-06-29	Enrico Tassi	...	tree \| commitdiff
2009-06-29	Enrico Tassi	do not infer on closed goals	tree \| commitdiff
2009-06-29	Enrico Tassi	...	tree \| commitdiff
2009-06-29	denes	First attempt for refined goal selection strategy	tree \| commitdiff
2009-06-29	Enrico Tassi	added (but not active) last chance idea	tree \| commitdiff
2009-06-29	denes	Implemented orphan murdering technique	tree \| commitdiff
2009-06-29	Enrico Tassi	new make test target	tree \| commitdiff
2009-06-26	Andrea Asperti	attempt to run a last chance procedure after the timeout	tree \| commitdiff
2009-06-26	Andrea Asperti	the timeout is passed to test last chance	tree \| commitdiff
2009-06-26	Andrea Asperti	this case is not assert false since it can happen if...	tree \| commitdiff
2009-06-26	Andrea Asperti	fixed parsing	tree \| commitdiff
2009-06-26	Andrea Asperti	convenient problem lists	tree \| commitdiff
2009-06-26	Andrea Asperti	an easy for loop	tree \| commitdiff
2009-06-26	Andrea Asperti	deep subsumption activated	tree \| commitdiff
2009-06-26	denes	Implemented orphan murder test (clauses are not discard...	tree \| commitdiff
next

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

RSS Atom