From ce7c528298b045b7363d530a8db034aeb622cd42 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 1 Apr 2018 01:35:06 +0200
Subject: [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.
---
 intf/vernacexpr.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index e029c78e49..767263d20f 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].*)
-- 
cgit v1.2.3