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

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

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

2005-07-22	Alberto Griggio	added optional "paramodulation" parameter to auto to...	blob \| commitdiff \| raw
2005-07-21	Alberto Griggio	if paramodulation fails, go on with the normal auto...	blob \| commitdiff \| raw \| diff to current
2005-07-21	Alberto Griggio	integration with paramodulation	blob \| commitdiff \| raw \| diff to current
2005-07-07	Enrico Tassi	fixed auto when the context has some deleted hypothesis	blob \| commitdiff \| raw \| diff to current
2005-07-06	Enrico Tassi	now it doesn't try to apply a cleared hypothesis	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	* auto_tac removed (it can be found in CVS)	blob \| commitdiff \| raw \| diff to current
2005-06-27	Enrico Tassi	fixed LApply pretty printing	blob \| commitdiff \| raw \| diff to current
2005-06-24	Claudio Sacerdoti...	New implementation of experimental_hint/auto (called...	blob \| commitdiff \| raw \| diff to current
2005-06-23	Enrico Tassi	Much simpler (and slightly more performant) implementat...	blob \| commitdiff \| raw \| diff to current
2005-06-16	Claudio Sacerdoti...	Locally implemented print_context replaced by CicPp...	blob \| commitdiff \| raw \| diff to current
2005-06-16	Andrea Asperti	A cleaned version of auto_tac_new.	blob \| commitdiff \| raw \| diff to current
2005-06-16	Stefano Zacchiroli	added depth and width (optional) parameters to auto_tac_new	blob \| commitdiff \| raw \| diff to current
2005-06-10	Claudio Sacerdoti...	Got rid of a few warnings.	blob \| commitdiff \| raw \| diff to current
2005-05-27	Enrico Tassi	removed debug prerr_endline	blob \| commitdiff \| raw \| diff to current
2005-05-03	Andrea Asperti	First version of instance.	blob \| commitdiff \| raw \| diff to current
2005-05-02	Enrico Tassi	attached auto	blob \| commitdiff \| raw \| diff to current
2004-12-06	Andrea Asperti	New version of auto with "width".	blob \| commitdiff \| raw \| diff to current
2004-11-30	Andrea Asperti	Bug in the management of substitutions into auto corrected.	blob \| commitdiff \| raw \| diff to current
2004-11-04	Andrea Asperti	Auto moved to a new file autoTactic.ml	blob \| commitdiff \| raw \| diff to current

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

RSS Atom