diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 19:10:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 19:54:00 +0200 |
| commit | 0fd7d060e0872a6ae3662dfb7a1fb940b80ef9df (patch) | |
| tree | 579953b20f35220b07e876f1b114c20e32e8c498 /vernac/topfmt.mli | |
| parent | da0d6da035206778c1d99ef51f471b4b22016492 (diff) | |
[toplevel] Don't check proofs in -quick mode.
This fixes a logical error introduced in
ce2b2058587224ade9261cd4127ef4f6e94d356b
Patch by @gares, closes https://coq.inria.fr/bugs/show_bug.cgi?id=5484
Diffstat (limited to 'vernac/topfmt.mli')
0 files changed, 0 insertions, 0 deletions