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.
---
 plugins/decl_mode/g_decl_mode.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

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