]> matita.cs.unibo.it Git - helm.git/commit
backport of patches to unification
authorEnrico Tassi <enrico.tassi@inria.fr>
Sun, 17 Oct 2010 09:12:29 +0000 (09:12 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sun, 17 Oct 2010 09:12:29 +0000 (09:12 +0000)
commit2e6a92bad35a8f8883c498c6a2f36ea3208d4ddd
tree7e9c4f55d84d0b968e8c210cc817e5e5e59c3f86
parentc6ee1124bbfd9ecf01ed5fd5b92e0b32b2c47d97
backport of patches to unification
matita/components/ng_paramodulation/orderings.ml
matita/components/ng_refiner/nCicMetaSubst.ml
matita/components/ng_refiner/nCicMetaSubst.mli
matita/components/ng_refiner/nCicUnification.ml