]> matita.cs.unibo.it Git - helm.git/commit
superposition_left not performed if the input goal is an identity
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 28 Jun 2006 10:28:58 +0000 (10:28 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 28 Jun 2006 10:28:58 +0000 (10:28 +0000)
commitc515304b306f38ae7387aff6fe44e36fa9e7bfa5
treeaea8276475941997040af6bc344489dab29eb8a3
parentaf44f0cf5173825eb0cadd1967424315cebe9076
superposition_left not performed if the input goal is an identity
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/saturation.ml