diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-23 13:46:43 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 05:48:44 -0400 |
| commit | 8baf120d5cf5045d188f7d926162643a6e7ebcd0 (patch) | |
| tree | c84ad72f9afc6c70c204626b40a00c6608bfd071 /stm/proofBlockDelimiter.mli | |
| parent | f6cea698f19766087fa56b16ed8dc8cedf079643 (diff) | |
STM: proof block detection for par:
"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
Diffstat (limited to 'stm/proofBlockDelimiter.mli')
| -rw-r--r-- | stm/proofBlockDelimiter.mli | 2 |
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 + |