]> 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)
commit356f9fafa095801f1be70ff495f0977ce96ed6bc
tree4b9b33a947ecc92fbd8a91ba7d12d92d21764b8e
parent25835a1eac5698fedca50ebae1e18bef49a67c87
- code cleanup, especialli in Indexing where all the goal related functions have
  been revised
- proofs are now factorized with LetIn
- support for profiling
components/tactics/paramodulation/equality.ml
components/tactics/paramodulation/equality.mli
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/indexing.mli
components/tactics/paramodulation/inference.ml
components/tactics/paramodulation/inference.mli
components/tactics/paramodulation/saturation.ml
components/tactics/paramodulation/saturation.mli
components/tactics/paramodulation/subst.ml
components/tactics/paramodulation/subst.mli