]> matita.cs.unibo.it Git - helm.git/commit
The declarative rewriting step now tries auto timeout=3 before
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Apr 2007 15:33:27 +0000 (15:33 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Apr 2007 15:33:27 +0000 (15:33 +0000)
commit20fcf3075628a59f30db4cc3ce81ea0d0f410d3f
treebbfed381c1bfe7c7a21814a44a912eb7a0dc1111
parent7adc1d3082ee8d50e236a549a2c341b96becf1fe
The declarative rewriting step now tries auto timeout=3 before
auto paramodulation timeout=3. This seems to work better then just
auto paramodulation alone when the user tries to help the system.
This because paramodulation is more confused than helped.
helm/software/components/tactics/declarative.ml
helm/software/components/tactics/tactics.mli