]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8f7fd6b) | 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)
commitcec2e3fc6d110cb0c2996c104ca277fbee33bb9e
tree384a7334ae0801e178875e61238597e057814d2atree | snapshot
parent8f7fd6bb8082590c9360e9197c7cd9d9d32b7a63commit | diff
before goals are inferred with current,
we demodulate them with active+current
(was: only with current)
components/tactics/paramodulation/saturation.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.