diff options
| author | Emilio Jesus Gallego Arias | 2017-04-24 19:10:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-24 19:54:00 +0200 |
| commit | 0fd7d060e0872a6ae3662dfb7a1fb940b80ef9df (patch) | |
| tree | 579953b20f35220b07e876f1b114c20e32e8c498 | |
| 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
| -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 19753b6f64..f81f77e6ec 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. *) |