]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a41f941) | patch
demodulation of goal activated again.
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 19 Jun 2006 14:44:11 +0000 (14:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 19 Jun 2006 14:44:11 +0000 (14:44 +0000)
commite4158685ac9f6a89c0e208d7c3c0faed84ae45fc
treeb1c6fc73872651f031e126094dda2295f0cc1ac2tree | snapshot
parenta41f941ef133b7b8dcdf306d63f43f7bfb8d5275commit | diff
demodulation of goal activated again.
to deactivate it, the check_if_goal_set_us_solved should be moved after the infeer_goal step
helm/software/components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.