diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-22 00:23:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-24 14:18:18 +0100 |
| commit | 584a832d4f681d34c7cbdd87d9ceb7a742b39959 (patch) | |
| tree | 1030c2c5a0a3dbfdb2b08773f2ca56ab80cde835 /intf | |
| parent | 530cd175c1b7465c3fa35c300f42b022bed9b25b (diff) | |
[stm] Remove some obsolete vernacs/classification.
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 17 |
1 files changed, 4 insertions, 13 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8827bc132..f782dd639 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -283,14 +283,9 @@ type bullet = | Plus of int (** {6 Types concerning Stm} *) -type 'a stm_vernac = +type 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} *) @@ -450,8 +445,9 @@ type vernac_expr = | VernacRegister of lident * register_kind | VernacComments of comment list - (* Stm backdoor *) - | VernacStm of vernac_expr stm_vernac + (* Stm backdoor: used in fake_id, will be removed when fake_ide + becomes aware of feedback about completed jobs. *) + | VernacStm of stm_vernac (* Proof management *) | VernacGoal of constr_expr @@ -509,16 +505,11 @@ and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) 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_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].*) |