diff options
| author | Enrico Tassi | 2016-05-23 11:11:30 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-06 05:48:44 -0400 |
| commit | 5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 (patch) | |
| tree | c803222d842bd96f3a25852633288e3aab14f45f /intf | |
| parent | 07115d044cb97bc6c0a7323783d4d53e083d3e89 (diff) | |
STM: proof block detection/error resilience API
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
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 |