diff options
| author | Théo Zimmermann | 2020-05-25 15:05:28 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-25 18:50:47 +0200 |
| commit | 488cd018153a13fd9136415751c57d48c7ac7d5c (patch) | |
| tree | 1b01ec95f390ab9f2a0284e77016709d8749a292 /kernel/nativelambda.mli | |
| parent | 16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (diff) | |
Fix output tests for location errors when running in async mode.
In this mode, an additional error was emitted, which made the test fail:
Error: There are pending proofs: Unnamed_thm.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions