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.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'API/API.mli')

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