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.
---
 intf/vernacexpr.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 3cb1a311f8..ea412a7d6a 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -502,7 +502,6 @@ type vernac_type =
   | VtProofStep of proof_step
   | VtProofMode of string
   | VtQuery of vernac_part_of_script * Feedback.route_id
-  | VtBack of vernac_part_of_script * Stateid.t
   | VtMeta
   | VtUnknown
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
-- 
cgit v1.2.3