]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 33b1f57) | patch
1) variables occurring only in proofs anre not relocated
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 26 May 2006 11:08:29 +0000 (11:08 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 26 May 2006 11:08:29 +0000 (11:08 +0000)
commit0f8a03b999acc2a16cbbffd6b19ab0e2967587cc
treec6a7c7e2519dd19a825ee323cb73013d132d7039tree | snapshot
parent33b1f57feafa53d0520035f3a27f6c18c36f478dcommit | diff
1) variables occurring only in proofs anre not relocated
2) during unification the resulting metasenv is cleaned of duplicates
   (duplicates can only be variables in proofs, not in left/right)
components/tactics/paramodulation/equality.ml diff | blob | history
components/tactics/paramodulation/indexing.ml diff | blob | history
components/tactics/paramodulation/inference.ml diff | blob | history
components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.