diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:08:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:24 +0200 |
| commit | 467db5040fe2f311f8f5493f89dc8f95647a9a0b (patch) | |
| tree | 5ebbe4139abc44bbef7362aa860c57711d6dcfd9 /printing/ppvernac.ml | |
| parent | 8e3c749e69649fb45750355e464ce7c16a4462c7 (diff) | |
Uncountably many bullets (+,-,*,++,--,**,+++,...).
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 263cc6a17..d01e6a028 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -953,9 +953,9 @@ let rec pr_vernac = function str "with" ++ spc() ++pr_raw_tactic te | VernacProofMode s -> str ("Proof Mode "^s) | VernacBullet b -> begin match b with - | Dash -> str"-" - | Star -> str"*" - | Plus -> str"+" + | Dash n -> str (String.make n '-') + | Star n -> str (String.make n '*') + | Plus n -> str (String.make n '+') end ++ spc() | VernacSubproof None -> str "{" | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i |