aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--stm/vernac_classifier.ml2
1 files changed, 1 insertions, 1 deletions
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