summaryrefslogtreecommitdiff
path: root/stm/proofBlockDelimiter.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/proofBlockDelimiter.mli')
-rw-r--r--stm/proofBlockDelimiter.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 9784de11..eacd3687 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -38,6 +38,6 @@ val crawl :
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
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t