aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-24 19:10:19 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-24 19:54:00 +0200
commit0fd7d060e0872a6ae3662dfb7a1fb940b80ef9df (patch)
tree579953b20f35220b07e876f1b114c20e32e8c498 /toplevel
parentda0d6da035206778c1d99ef51f471b4b22016492 (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.ml4
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. *)