From ab53757a3bf57ced503023f3cf9dea5b5503dfea Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 17:12:51 +0200
Subject: [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.
---
 API/API.ml  | 1 +
 API/API.mli | 6 +++++-
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'API')

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
-- 
cgit v1.2.3