diff options
| author | Hugo Herbelin | 2020-04-12 14:46:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-12 14:46:41 +0200 |
| commit | 0d207dc4dc7d593c422ed81c07a7e1532899e4ec (patch) | |
| tree | 9e2d656e7c66dbf9c3e377a695312d3cab28114a /test-suite/output/ErrorInModule.v | |
| parent | afb4173e71f6069f7a49baf44b16569bf0cbcce4 (diff) | |
Exporting BEST as OPT for the tests using coq_makefile-generated Makefile.
Diffstat (limited to 'test-suite/output/ErrorInModule.v')
0 files changed, 0 insertions, 0 deletions