diff options
| author | Enrico Tassi | 2016-06-14 10:51:00 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-14 10:51:00 +0200 |
| commit | ff67a511a358ada3daefea0839e18d474531e13d (patch) | |
| tree | b5dfb7b8d79394d1aabbe0d125d30e12a0fbf621 /intf | |
| parent | 19330a458b907b5e66a967adbfe572d92194913c (diff) | |
| parent | 1334a657052a2385c3f3b01cc65c3ccae448fa96 (diff) | |
Merge remote-tracking branch 'origin/pr/173' into trunk
This is the "error resiliency" mode for STM
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ae9328fcc0..6ce15a7c5a 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -454,7 +454,7 @@ type vernac_type = | VtStartProof of vernac_start | VtSideff of vernac_sideff_type | VtQed of vernac_qed_type - | VtProofStep of bool (* parallelize *) + | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * report_with | VtStm of vernac_control * vernac_part_of_script @@ -476,6 +476,11 @@ and vernac_control = and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and proof_step = { (* TODO: inline with OCaml 4.03 *) + parallel : bool; + proof_block_detection : proof_block_name option +} +and proof_block_name = string (* open type of delimiters *) type vernac_when = | VtNow | VtLater |