diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-01 01:35:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-01 01:35:06 +0200 |
| commit | ce7c528298b045b7363d530a8db034aeb622cd42 (patch) | |
| tree | 97a858abf220c511d1303130323bf5fbfd6d47c8 /intf | |
| parent | 8b15eee6125f7f8596f17e9c982fb944a5e3f9be (diff) | |
[stm] More cleanup of "classification is not an interpreter"
We remove meta-information from the query classification and we don't
process `Stm.query` as a transaction anymore, as the right API is
available to it to execute the command directly.
This simplifies pure commands and removes some impossible cases.
Depends on #7138.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index e029c78e4..767263d20 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -505,14 +505,13 @@ type vernac_type = | VtProofMode of string (* Queries are commands assumed to be "pure", that is to say, they don't modify the interpretation state. *) - | VtQuery of vernac_part_of_script * Feedback.route_id + | VtQuery (* To be removed *) | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list -and vernac_part_of_script = bool and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) |