]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 30da02e) | 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)
commit126e56fc8eb4096f8c133258e5d43f82305ebd0b
treeda6c5bed451507f0e93e16bfe412851dd4d447datree | snapshot
parent30da02e8be0612dac41b435bc7e8a9bea41cc352commit | diff
demodulation of goal activated again.
to deactivate it, the check_if_goal_set_us_solved should be moved after the infeer_goal step
components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.