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 /plugins/decl_mode | |
| 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 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 78a95143df..4c3bebd65f 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -98,7 +98,7 @@ let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr let classify_proof_instr = function | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow - | _ -> VtProofStep false, VtLater + | _ -> Vernac_classifier.classify_as_proofstep (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. |