From fca82378cd2824534383f1f5bc09d08fade1dc17 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 24 Apr 2018 18:21:49 +0200
Subject: [api] Move bullets and goals selectors to `proofs/`

`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.

In particular, we move:

- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
---
 stm/proofBlockDelimiter.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm/proofBlockDelimiter.mli')

diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 9784de1141..eacd3687ae 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
 
-- 
cgit v1.2.3