]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics/autoTactic.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / tactics / autoTactic.ml
2005-10-25 Claudio Sacerdoti... Every exception that used to have type string is now...
2005-09-26 Alberto Griggionew signature of auto_tac, with a new optional argument...
2005-09-23 Claudio Sacerdoti... New module HMysql (to abstract over Mysql and make...
2005-09-21 Claudio Sacerdoti... All the debug_print are now lazy.
2005-09-19 Claudio Sacerdoti... Profiling code commented out.
2005-07-22 Alberto Griggioadded optional "paramodulation" parameter to auto to...
2005-07-21 Alberto Griggioif paramodulation fails, go on with the normal auto...
2005-07-21 Alberto Griggiointegration with paramodulation
2005-07-07 Enrico Tassifixed auto when the context has some deleted hypothesis
2005-07-06 Enrico Tassinow it doesn't try to apply a cleared hypothesis
2005-06-27 Claudio Sacerdoti... * auto_tac removed (it can be found in CVS)
2005-06-27 Enrico Tassifixed LApply pretty printing
2005-06-24 Claudio Sacerdoti... New implementation of experimental_hint/auto (called...
2005-06-23 Enrico TassiMuch simpler (and slightly more performant) implementat...
2005-06-16 Claudio Sacerdoti... Locally implemented print_context replaced by CicPp...
2005-06-16 Andrea AspertiA cleaned version of auto_tac_new.
2005-06-16 Stefano Zacchiroliadded depth and width (optional) parameters to auto_tac_new
2005-06-10 Claudio Sacerdoti... Got rid of a few warnings.
2005-05-27 Enrico Tassiremoved debug prerr_endline
2005-05-03 Andrea AspertiFirst version of instance.
2005-05-02 Enrico Tassiattached auto
2004-12-06 Andrea AspertiNew version of auto with "width".
2004-11-30 Andrea AspertiBug in the management of substitutions into auto corrected.
2004-11-04 Andrea AspertiAuto moved to a new file autoTactic.ml