From d9704f80a4f4b565f77368dbf7c9650d301a233d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Oct 2017 12:54:57 +0200 Subject: [stm] Remove VtBack from public classification. We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away. --- stm/vernac_classifier.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'stm/vernac_classifier.ml') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index e5d197eb1..3aa2cd707 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -31,7 +31,6 @@ let string_of_vernac_type = function Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route - | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b | VtMeta -> "Meta " let string_of_vernac_when = function @@ -73,7 +72,7 @@ let rec classify_vernac e = | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtBack _ | VtProofMode _ | VtMeta), _ as x -> x + | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow -- cgit v1.2.3