diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-05 09:48:36 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-05 09:48:36 +0200 |
| commit | f97498a6c104da9b7b31f84505db76194a566f9b (patch) | |
| tree | 857eae2c889de03a65cf5ba02441542865f1d1fb /intf | |
| parent | b7aa3064e50e34afe2e1a458f61e6e2b1f5d37f8 (diff) | |
| parent | ce7c528298b045b7363d530a8db034aeb622cd42 (diff) | |
Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"
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 0e84a07aa..76b35b08f 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -501,14 +501,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].*) |