]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1cb502b) | 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)
commit1d973a067d441fbae43905abb704e21faa223e2b
tree5a7c6c9e6f1fefe7a2e7dfe6cdb44ecceec7c80dtree | snapshot
parent1cb502bc3e0c797bf9b4c92c75a849f44df687ebcommit | 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)
helm/software/components/tactics/paramodulation/equality.ml diff | blob | history
helm/software/components/tactics/paramodulation/indexing.ml diff | blob | history
helm/software/components/tactics/paramodulation/inference.ml diff | blob | history
helm/software/components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.