]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bf0b308) | patch
- patch to consider the symbols of the goal when computing the weight of an
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 3 Jul 2006 11:48:44 +0000 (11:48 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 3 Jul 2006 11:48:44 +0000 (11:48 +0000)
commitae47205236492ae4271586cdf75a25597304da1e
tree47cb37e3f69a8192cc7092d015aa192ffa0575fatree | snapshot
parentbf0b308923fbe96bdd4bd8ee0f4495958211ab6fcommit | diff
- patch to consider the symbols of the goal when computing the weight of an
  equality.
- actives simplified during fwd/back are not appended (but put in front) of the
  passive list
components/tactics/paramodulation/saturation.ml diff | blob | history
components/tactics/paramodulation/utils.ml diff | blob | history
components/tactics/paramodulation/utils.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.