diff options
author | Eelco Dolstra <e.dolstra@tudelft.nl> | 2003-07-04T15·29+0000 |
---|---|---|
committer | Eelco Dolstra <e.dolstra@tudelft.nl> | 2003-07-04T15·29+0000 |
commit | 01b34fe5843df9888737699ee9f9fe2f161a1fa3 (patch) | |
tree | aceb2e7be03951e20d4af2f8d666f957f6925d47 /src/globals.hh | |
parent | 207ff2caf0f48db0fb539e228ec5c3938a279f2a (diff) |
* Cleanup.
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 |