matita.cs.unibo.it Git - helm.git/history - components/tactics/autoTactic.ml

]> matita.cs.unibo.it Git - helm.git/history - components/tactics/autoTactic.ml

[helm.git] / components / tactics / autoTactic.ml

2007-05-17	Enrico Tassi	added a (for the moment) dummy field _subst to Proofeng...	blob \| commitdiff \| raw
2007-01-10	Ferruccio Guidi	attributes now in the proof status: commit 2	blob \| commitdiff \| raw \| diff to current
2006-11-23	Andrea Asperti	Modifications to auto due to the introduction of the...	blob \| commitdiff \| raw \| diff to current
2006-10-30	Claudio Sacerdoti...	Debugging code is now controlled by the debug flag.	blob \| commitdiff \| raw \| diff to current
2006-10-10	Claudio Sacerdoti...	Sorry, bug introduced by me yesterday now fixed.	blob \| commitdiff \| raw \| diff to current
2006-10-09	Claudio Sacerdoti...	1. applyS now uses its ~params	blob \| commitdiff \| raw \| diff to current
2006-10-06	Enrico Tassi	resumed ol auto	blob \| commitdiff \| raw \| diff to current
2006-10-02	Enrico Tassi	auto always uses the context (even if paramodulation...	blob \| commitdiff \| raw \| diff to current
2006-10-01	Enrico Tassi	when use_only_paramod is true do not calculate the...	blob \| commitdiff \| raw \| diff to current
2006-09-29	Enrico Tassi	new version of auto that is able to prove the irrationa...	blob \| commitdiff \| raw \| diff to current
2006-09-27	Enrico Tassi	auto snapshot	blob \| commitdiff \| raw \| diff to current
2006-09-21	Enrico Tassi	auto snapshot	blob \| commitdiff \| raw \| diff to current
2006-07-24	Enrico Tassi	added timeout parameter to auto paramodulation.	blob \| commitdiff \| raw \| diff to current
2006-07-22	Enrico Tassi	matitaprover	blob \| commitdiff \| raw \| diff to current
2006-06-27	Enrico Tassi	using the new metadataConstraint function	blob \| commitdiff \| raw \| diff to current
2006-06-26	Enrico Tassi	more work for the generic auto parameters	blob \| commitdiff \| raw \| diff to current
2006-06-21	Enrico Tassi	added the geniric	blob \| commitdiff \| raw \| diff to current
2006-06-15	Andrea Asperti	added applyS	blob \| commitdiff \| raw \| diff to current
2006-05-31	Enrico Tassi	fixed proofs, contextualization should now work.	blob \| commitdiff \| raw \| diff to current
2006-05-29	Enrico Tassi	profilings are printed	blob \| commitdiff \| raw \| diff to current
2006-04-26	Enrico Tassi	added a new type for proofs.	blob \| commitdiff \| raw \| diff to current
2006-02-03	Stefano Zacchiroli	- renamed ocaml/ to components/	blob \| commitdiff \| raw \| diff to current

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

RSS Atom