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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 19753b6f6..f81f77e6e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -123,7 +123,9 @@ let rec interp_vernac sid po (loc,com) = (* Due to bug #5363 we cannot use observe here as we should, it otherwise reveals bugs *) (* Stm.observe nsid; *) - Stm.finish (); + + let check_proof = Flags.(!compilation_mode = BuildVo || not !batch_mode) in + if check_proof then Stm.finish (); (* We could use a more refined criteria that depends on the vernac. For now we imitate the old approach. *) |