aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/proofBlockDelimiter.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/proofBlockDelimiter.mli')
-rw-r--r--stm/proofBlockDelimiter.mli2
1 files changed, 2 insertions, 0 deletions
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
+