]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 48aa99d) | patch
before goals are inferred with current,
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 29 Jun 2006 11:17:46 +0000 (11:17 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 29 Jun 2006 11:17:46 +0000 (11:17 +0000)
commita004949b379723275993bbbda15b004908572871
treedbc85161fcf2888ce22b2785b49ce1aa83b67f4atree | snapshot
parent48aa99d1d9659e55d68ab3ef50b10bc6165eee03commit | diff
before goals are inferred with current,
we demodulate them with active+current
(was: only with current)
helm/software/components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.