diff options
| author | Théo Zimmermann | 2018-05-02 15:04:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-02 15:04:57 +0200 |
| commit | fd146ca38202c9843b4240cbdac0ae75f57e4d67 (patch) | |
| tree | 39f0c957c4ea02e6976299b4183b6bcfa8ea9f7a /stm/proofBlockDelimiter.mli | |
| parent | 48ec42bb91b8c0fb4d5930e62e29a408de594482 (diff) | |
| parent | fca82378cd2824534383f1f5bc09d08fade1dc17 (diff) | |
Merge PR #7339: [api] Move bullets and goals selectors to `proofs/`
Diffstat (limited to 'stm/proofBlockDelimiter.mli')
| -rw-r--r-- | stm/proofBlockDelimiter.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 |