]> 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)
commita0cb7cf4ac234997157aac20a1a68a4a88e805e1
treefab7bf49bd67be51cac2af189852fd8fcad03d87
parent818e4b4f4812ddb42a4647a205e4d14c0793b6aa
superposition_left not performed if the input goal is an identity
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/saturation.ml