]> matita.cs.unibo.it Git - helm.git/history - components/tactics/auto.ml
Even if we are at depth 0, we first check in the cache for a solution,
[helm.git] / components / tactics / auto.ml
2007-04-30 Andrea AspertiEven if we are at depth 0, we first check in the cache...
2007-04-30 Andrea AspertiRemoved an assert false; everything works again, but...
2007-04-27 Andrea AspertiSubst is passed in input to apapluy, so no need to...
2007-02-09 Claudio Sacerdoti... Debugging code fixed. To enable debugging just set...
2007-01-10 Ferruccio Guidiattributes now in the proof status: commit 2
2006-12-29 Ferruccio Guidi- tactics:
2006-12-14 Claudio Sacerdoti... Huge commit:
2006-11-29 Andrea AspertiDemodulate_tac now depends on the universe
2006-11-27 Andrea AspertiOnly modified for taking unfold into account.
2006-11-23 Andrea AspertiModifications to auto due to the introduction of the...
2006-10-25 Andrea AspertiAdded a couple of flags to auto
2006-10-20 Andrea AspertiMajor changes to auto, documented on the helm mailing...
2006-10-12 Enrico Tassitimeout if unspecfied should be set to infinity, not...
2006-10-12 Claudio Sacerdoti... The default for paramodulation is now back to false...
2006-10-11 Claudio Sacerdoti... My previous commit changed the regular timeout of param...
2006-10-09 Claudio Sacerdoti... 1. applyS now uses its ~params
2006-10-09 Claudio Sacerdoti... applyS now receives the same parameters that auto receives.
2006-10-03 Andrea AspertiChanged auto from implicit to option and renamed a...
2006-10-02 Enrico Tassi50 steps on goal are fine for irrat2
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