From 22c9cb140157ae47a52d0321ffa4a98b9c909305 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 22 Nov 2018 07:57:17 +0100
Subject: Fix vernac classification of `Fail Instance`

AFAIK `Fail Instance` cannot open a goal.
---
 stm/vernac_classifier.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f40b3e901b..454a4b66e7 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -214,6 +214,6 @@ let classify_vernac e =
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtNow
-        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+        | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater)
   in
   static_control_classifier e
-- 
cgit v1.2.3