]> matita.cs.unibo.it Git - helm.git/commit
fixed infer_goal, added simplification before inferring with current
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 27 Jun 2006 16:55:52 +0000 (16:55 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 27 Jun 2006 16:55:52 +0000 (16:55 +0000)
commit44f4e888646ac95752bbd8c3e7b9b4b48209b1a6
treedb2b4a6815a9252e55c70ae77f915aa0e0564797
parenta507a21ca97552dec5077667cf8433f24d7a45ae
fixed infer_goal, added simplification before inferring with current
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/saturation.mli