diff options
| author | Gaëtan Gilbert | 2019-04-02 14:37:37 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-02 15:23:46 +0200 |
| commit | 2f1111e4349c41e2d750795475241b919edc1fb6 (patch) | |
| tree | fbc19b0dbb0366f645de19d3db0af0834cfdd373 /dev | |
| parent | 772b2d1e61d7af71c3e7f81d857fd5c945e9ffb8 (diff) | |
coqchk: don't marshal opaques for dependencies of -norec libraries
About 20% better perf on test-suite/arithmetic/mod (3.4s to 2.6s)
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions