]> matita.cs.unibo.it Git - helm.git/commit
- code cleanup, especialli in Indexing where all the goal related functions have
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 22 May 2006 15:06:42 +0000 (15:06 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 22 May 2006 15:06:42 +0000 (15:06 +0000)
commit942023d1f147318b7869f40fb1556c2d69f3d731
treecac9f3a6c93d2d85ea5784ff79d23a0d4159fd54
parentaaa3e96cdef325732c756ddf6ad20915b1587d93
- code cleanup, especialli in Indexing where all the goal related functions have
  been revised
- proofs are now factorized with LetIn
- support for profiling
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/paramodulation/equality.mli
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/indexing.mli
helm/software/components/tactics/paramodulation/inference.ml
helm/software/components/tactics/paramodulation/inference.mli
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/saturation.mli
helm/software/components/tactics/paramodulation/subst.ml
helm/software/components/tactics/paramodulation/subst.mli