]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/autoTactic.ml
- transcript: patched to generate CoRN_notation.ma instead of CoRN.ma
[helm.git] / helm / software / components / tactics / autoTactic.ml
2006-10-30 Claudio Sacerdoti... Debugging code is now controlled by the debug flag.
2006-10-10 Claudio Sacerdoti... Sorry, bug introduced by me yesterday now fixed.
2006-10-09 Claudio Sacerdoti... 1. applyS now uses its ~params
2006-10-06 Enrico Tassiresumed ol auto
2006-10-02 Enrico Tassiauto always uses the context (even if paramodulation...
2006-10-01 Enrico Tassiwhen use_only_paramod is true do not calculate the...
2006-09-29 Enrico Tassinew version of auto that is able to prove the irrationa...
2006-09-27 Enrico Tassiauto snapshot
2006-09-21 Enrico Tassiauto snapshot
2006-07-24 Enrico Tassiadded timeout parameter to auto paramodulation.
2006-07-22 Enrico Tassimatitaprover
2006-06-27 Enrico Tassiusing the new metadataConstraint function
2006-06-26 Enrico Tassimore work for the generic auto parameters
2006-06-21 Enrico Tassiadded the geniric
2006-06-15 Andrea Aspertiadded applyS
2006-05-31 Enrico Tassifixed proofs, contextualization should now work.
2006-05-29 Enrico Tassiprofilings are printed
2006-04-26 Enrico Tassiadded a new type for proofs.
2006-02-03 Stefano Zacchiroli- renamed ocaml/ to components/