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.
---
 API/API.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index e518cf583f..535f6a29bb 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3713,7 +3713,6 @@ sig
                    | 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 =
-- 
cgit v1.2.3