From ab915f905ca81018521db63cdd0f3126b35c69c6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Oct 2017 19:21:00 +0200
Subject: [stm] First step to move interpretation of Undo commands out of the
 classifier.

The vernacular classifier has a current special case for "Undo" like
commands, as it needs access to the document structure in order to
produce the proper "VtBack" classification, however the classifier is
defined before the document is.

We introduce a new delegation status `VtMeta` that allows us to
interpreted such commands outside the classifier itself.
---
 API/API.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 879323a37d..e518cf583f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3714,6 +3714,7 @@ sig
                    | 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
-- 
cgit v1.2.3