From 0fd7d060e0872a6ae3662dfb7a1fb940b80ef9df Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 24 Apr 2017 19:10:19 +0200
Subject: [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
---
 toplevel/vernac.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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. *)
-- 
cgit v1.2.3