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.
---
 printing/ppvernac.ml | 6 +++---
 printing/printer.ml  | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 781af47892..ca1499bc23 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -105,7 +105,7 @@ open Decl_kinds
         | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
   let pr_search a gopt b pr_p =
-    pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
+    pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
     ++
       match a with
       | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -490,7 +490,7 @@ open Decl_kinds
     | PrintVisibility s ->
       keyword "Print Visibility" ++ pr_opt str s
     | PrintAbout (qid,gopt) ->
-       pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
+       pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
        ++ keyword "About" ++ spc()  ++ pr_smart_global qid
     | PrintImplicit qid ->
       keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
@@ -1130,7 +1130,7 @@ open Decl_kinds
           | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
         in
         let pr_i = match io with None -> mt ()
-                               | Some i -> Proof_global.pr_goal_selector i ++ str ": " in
+                               | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in
         return (pr_i ++ pr_mayeval r c)
       | VernacGlobalCheck c ->
         return (hov 2 (keyword "Type" ++ pr_constrarg c))
diff --git a/printing/printer.ml b/printing/printer.ml
index 3c31dd96bf..58cfc2b885 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -798,7 +798,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
 	  | _ , _, _ ->
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
-              (let s = Proof_global.Bullet.suggest p in
+              (let s = Proof_bullet.suggest p in
                if Pp.ismt s then s else fnl () ++ s) ++
               fnl ()
             in
-- 
cgit v1.2.3