]> matita.cs.unibo.it Git - helm.git/commit
- proofs by subsumption now add a symmetry step if needed
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 29 May 2006 20:29:21 +0000 (20:29 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 29 May 2006 20:29:21 +0000 (20:29 +0000)
commit1b75bf92c6232210cb5fcce8683a7d6c0e7a3235
tree65a2d4757ffab7bbe537a4931294dc26f9bd9998
parentf340ae8d0be1c480c6a496a11157a6ccfb367c13
- proofs by subsumption now add a symmetry step if needed
- a little optimization for Equality.depend (just to aviod te exponenetial
  factor, but should be made faster)
- restored names in Lambda abstraction that give infos about the step they
  represent
components/tactics/paramodulation/equality.ml
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/indexing.mli
components/tactics/paramodulation/saturation.ml