diff options
| author | Maxime Dénès | 2017-09-18 13:27:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-19 11:43:42 +0200 |
| commit | 84accdaea3ce094cc5d0232107d3e2ea654a76c2 (patch) | |
| tree | eab140c332984b597536d1cabdf9b2ecd474b929 /API | |
| parent | d87bc5b9fb353655f8b905d73293abe96b0ad063 (diff) | |
Remove STM vernaculars.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/API/API.mli b/API/API.mli index 901ed3528b..50fbee5298 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3676,7 +3676,7 @@ sig | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtStm of vernac_control * vernac_part_of_script + | VtBack of vernac_part_of_script * Stateid.t | VtUnknown and vernac_qed_type = | VtKeep @@ -3685,10 +3685,6 @@ sig and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and vernac_part_of_script = bool - and vernac_control = - | VtWait - | VtJoinDocument - | VtBack of Stateid.t and opacity_guarantee = | GuaranteesOpacity | Doesn'tGuaranteeOpacity @@ -3770,7 +3766,6 @@ sig type option_value type showable type bullet - type stm_vernac type comment type register_kind type locatable @@ -3922,7 +3917,6 @@ sig | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list - | VernacStm of stm_vernac | VernacGoal of Constrexpr.constr_expr | VernacAbort of lident option | VernacAbortAll |