diff options
| author | Gaëtan Gilbert | 2019-03-26 23:22:40 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-26 23:24:43 +0100 |
| commit | 4220af0f8cfbf55bc0ce5fb2d3ddf8657a8807ed (patch) | |
| tree | 25ffbf22f85c251736b6c1910d9f3b0c72844784 /kernel/nativelib.mli | |
| parent | 2c37c0e7eea9b8406e534e93881158bb6919ed38 (diff) | |
Fix reproduction info for some past critical bugs
- test-suite/bugs/closed/xx.v renamed to .../bug_xx.v
- test-suite/failure/inductive4.v is now .../inductive.v
- repro for #4157 now added to the repo (it was in an unmerged commit
on @herbelin's repo)
- commit message of 244d7a9aa contains a repro for its bug (I didn't
bother adding to the test suite as a return of the bug could just as
well use different strings so the specific repro wouldn't test
anything useful)
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions