From 467db5040fe2f311f8f5493f89dc8f95647a9a0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 5 Aug 2014 19:08:48 +0200
Subject: Uncountably many bullets (+,-,*,++,--,**,+++,...).

---
 proofs/proof_global.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 96bc265fc2..52282375f7 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -386,16 +386,16 @@ module Bullet = struct
   exception FailedFocusBullet of t
 
   let bullet_eq b1 b2 = match b1, b2 with
-  | Vernacexpr.Dash, Vernacexpr.Dash -> true
-  | Vernacexpr.Star, Vernacexpr.Star -> true
-  | Vernacexpr.Plus, Vernacexpr.Plus -> true
+  | Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
+  | Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
+  | Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
   | _ -> false
 
   let pr_bullet b =
     match b with
-    | Vernacexpr.Dash -> str "-"
-    | Vernacexpr.Star -> str "*"
-    | Vernacexpr.Plus -> str "+"
+    | Vernacexpr.Dash n -> str (String.make n '-')
+    | Vernacexpr.Star n -> str (String.make n '*')
+    | Vernacexpr.Plus n -> str (String.make n '+')
 
   let _ = Errors.register_handler
     begin function
-- 
cgit v1.2.3