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 +
 1 file changed, 1 insertion(+)

(limited to 'API/API.ml')

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