diff options
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].*) |