diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index f77a940a7..92e4dd618 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -283,6 +283,16 @@ 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 *) @@ -441,6 +451,9 @@ 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 @@ -495,7 +508,7 @@ type vernac_type = | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * report_with - | VtBack of Stateid.t * vernac_part_of_script + | VtStm of vernac_control * 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 *) @@ -503,6 +516,14 @@ 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].*) |