diff options
| author | Emilio Jesus Gallego Arias | 2017-06-12 17:12:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-12 17:27:53 +0200 |
| commit | ab53757a3bf57ced503023f3cf9dea5b5503dfea (patch) | |
| tree | 97241209c0348d72fda82fa33d67095f39d32da3 /API | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
[proof] Move bullets to their own module.
Bullets were placed inside the `Proof_global` module, I guess that due
to the global registration function. However, it has logically nothing
to do with the functionality of `Proof_global` and the current
placement may create some interference between the developers
reworking proof state handling and bullets.
We thus put the bullet functionality into its own, independent file.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 1 | ||||
| -rw-r--r-- | API/API.mli | 6 |
2 files changed, 6 insertions, 1 deletions
diff --git a/API/API.ml b/API/API.ml index 2b7bbd561b..85e8f2e733 100644 --- a/API/API.ml +++ b/API/API.ml @@ -79,6 +79,7 @@ module Nametab = Nametab module Vernacentries = Vernacentries module Mltop = Mltop module Goal = Goal +module Proof_bullet = Proof_bullet module Proof_global = Proof_global module Proof = Proof module Smartlocate = Smartlocate diff --git a/API/API.mli b/API/API.mli index d844e8bf52..61da0c605d 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3376,6 +3376,11 @@ sig end end +module Proof_bullet : +sig + val get_default_goal_selector : unit -> Vernacexpr.goal_selector +end + module Proof_global : sig type proof_mode = Proof_global.proof_mode = { @@ -3410,7 +3415,6 @@ sig (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit val compact_the_proof : unit -> unit val register_proof_mode : proof_mode -> unit - val get_default_goal_selector : unit -> Vernacexpr.goal_selector exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof |