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.ml | |
| parent | 48ec42bb91b8c0fb4d5930e62e29a408de594482 (diff) | |
| parent | fca82378cd2824534383f1f5bc09d08fade1dc17 (diff) | |
Merge PR #7339: [api] Move bullets and goals selectors to `proofs/`
Diffstat (limited to 'stm/proofBlockDelimiter.ml')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 0af766219c..b8af2bcd56 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -23,8 +23,8 @@ val crawl : static_block_declaration option val unit_val : Stm.DynBlockData.t -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 val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control |