diff options
| author | Enrico Tassi | 2019-01-17 16:27:35 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-17 16:27:35 +0100 |
| commit | f50256c7b4a75a59bb25a78431f0b24ae1046bf3 (patch) | |
| tree | 0c9c7f4ff84957cd6f143d2b48ec4735ec7eced5 | |
| parent | 84e919a0969ff8dce44c6c5fb8bfd248f652e841 (diff) | |
| parent | 22c9cb140157ae47a52d0321ffa4a98b9c909305 (diff) | |
Merge PR #9048: Fix vernac classification of `Fail Instance`
Reviewed-by: gares
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
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 |