diff options
| author | Emilio Jesus Gallego Arias | 2017-10-16 12:54:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-10-17 02:18:29 +0200 |
| commit | d9704f80a4f4b565f77368dbf7c9650d301a233d (patch) | |
| tree | 793abaa0029376d87801f27f2d09309f6af92af2 /intf | |
| parent | ab915f905ca81018521db63cdd0f3126b35c69c6 (diff) | |
[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.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 *) |