diff options
| author | Emilio Jesus Gallego Arias | 2017-10-15 19:21:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-10-17 02:18:29 +0200 |
| commit | ab915f905ca81018521db63cdd0f3126b35c69c6 (patch) | |
| tree | 89846b34951330cdb4dcabaaad9d715afbb74173 /API/API.mli | |
| parent | c00cecfc66eb76d6bca8980ef719577fd81cc400 (diff) | |
[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.
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |