diff options
| author | Maxime Dénès | 2017-09-22 11:46:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-22 11:46:33 +0200 |
| commit | 06a723190858da8ed3f30736f22398aa7822c959 (patch) | |
| tree | 805ad45a4492a880dbf6008906eeaff807388ad0 /API | |
| parent | 63b3b3f307053fd055355d8a669456c988d083aa (diff) | |
| parent | 569e8f7601ee1484f8373320a102fa2ab026078c (diff) | |
Merge PR #1055: 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 |