From 5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 11:11:30 +0200
Subject: 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.
---
 intf/vernacexpr.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'intf')

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
-- 
cgit v1.2.3