From 8baf120d5cf5045d188f7d926162643a6e7ebcd0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 23 May 2016 13:46:43 +0200
Subject: STM: proof block detection for par:

"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
---
 stm/proofBlockDelimiter.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'stm/proofBlockDelimiter.mli')

diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 8455c1848..a55032a47 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -9,6 +9,7 @@
 (* This file implements proof block detection for:
    - blocks delimited by { and }
    - bullets with indentation
+   - par: terminator
 
    It exports utility functions to ease the development of other proof block
    detection code.
@@ -37,3 +38,4 @@ val unit_val : Stm.DynBlockData.t
 (* Bullets *)
 val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
 val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+
-- 
cgit v1.2.3