diff options
Diffstat (limited to 'src/globals.hh')
| -rw-r--r-- | src/globals.hh | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/globals.hh b/src/globals.hh index 8597ae2f89d7..8c6a763c48e3 100644 --- a/src/globals.hh +++ b/src/globals.hh @@ -21,7 +21,13 @@ extern string dbRefs; with hash h2. Note that a term $y$ is successor of $x$ iff there exists a - sequence of rewrite steps that rewrites $x$ into $y$. */ + sequence of rewrite steps that rewrites $x$ into $y$. + + Also note that instead of a successor, $y$ can be any term + equivalent to $x$, that is, reducing to the same result, as long as + $x$ is equal to or a successor of $y$. (This is useful, e.g., for + shared derivate caching over the network). +*/ extern string dbSuccessors; /* dbNetSources :: Hash -> URL |