diff options
| author | Hendrik Tews | 2020-06-19 22:39:26 +0200 |
|---|---|---|
| committer | Hendrik Tews | 2020-06-19 22:39:26 +0200 |
| commit | e81b4e3e3e9b15238ba6f9adf21ca0167cd83dcd (patch) | |
| tree | 3914f385c40e015538ee498d37d45ed65feab391 /pgshell | |
| parent | 0f0bb2c00fb7b20fd187cb92d4d2c3f84c4c5987 (diff) | |
coq-par-compile: use hash for ancestors
The hash avoids an exponentially growing number of duplicates in
the ancestor collection. Fixes #499
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions