Merge PR #770: [proof] Move bullets to their own module.

1 files changed, 2 insertions, 2 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8a647c6c18..9650ea19d7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1811,9 +1811,9 @@ let vernac_end_subproof () =
   Proof_global.simple_with_current_proof (fun _ p ->
     Proof.unfocus subproof_kind p ())
 
-let vernac_bullet (bullet:Proof_global.Bullet.t) =
+let vernac_bullet (bullet : Proof_bullet.t) =
   Proof_global.simple_with_current_proof (fun _ p ->
-    Proof_global.Bullet.put p bullet)
+    Proof_bullet.put p bullet)
 
 let vernac_show = let open Feedback in function
   | ShowScript -> assert false  (* Only the stm knows the script *)