]> matita.cs.unibo.it Git - helm.git/commit
goals after a superposition step are relocated
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 29 Jun 2006 10:01:16 +0000 (10:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 29 Jun 2006 10:01:16 +0000 (10:01 +0000)
commitd8d939cc3f78a805a3c16f715912ecd96c302592
tree326d5de5a9663de5c17a1d3a246ee644db81ba01
parentf68f452173a5077c58f93587faad65fcced77223
goals after a superposition step are relocated
components/tactics/paramodulation/equality.ml
components/tactics/paramodulation/equality.mli
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/indexing.mli
components/tactics/paramodulation/saturation.ml