diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-11-16 10:51:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-11-17 10:14:40 +0100 |
| commit | 26d180fa0b27edc773fd07c73906e4ed56475200 (patch) | |
| tree | 7b79952cd7221013f444dfdf8b3b9732be8365a1 /intf/vernacexpr.mli | |
| parent | 3a51aa7265f35dd3cbf3f7bff858d663e4406146 (diff) | |
[stm] Remove STM-related vernaculars
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 23 |
1 files changed, 1 insertions, 22 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 92e4dd618..f77a940a7 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -283,16 +283,6 @@ type bullet = | Star of int | Plus of int -(** {6 Types concerning Stm} *) -type 'a stm_vernac = - | JoinDocument - | Finish - | Wait - | PrintDag - | Observe of Stateid.t - | Command of 'a (* An out of flow command not to be recorded by Stm *) - | PGLast of 'a (* To ease the life of PG *) - (** {6 Types concerning the module layer} *) (** Rigid / flexible module signature *) @@ -451,9 +441,6 @@ type vernac_expr = | VernacRegister of lident * register_kind | VernacComments of comment list - (* Stm backdoor *) - | VernacStm of vernac_expr stm_vernac - (* Proof management *) | VernacGoal of constr_expr | VernacAbort of lident option @@ -508,7 +495,7 @@ type vernac_type = | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * report_with - | VtStm of vernac_control * vernac_part_of_script + | VtBack of Stateid.t * vernac_part_of_script | VtUnknown and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) @@ -516,14 +503,6 @@ and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list and vernac_is_alias = bool and vernac_part_of_script = bool -and vernac_control = - | VtFinish - | VtWait - | VtJoinDocument - | VtPrintDag - | VtObserve of Stateid.t - | VtBack of Stateid.t - | VtPG and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) |