diff options
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e5f3d58644..7ba1f44392 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1196,7 +1196,7 @@ module Make | Dash n -> str (String.make n '-') | Star n -> str (String.make n '*') | Plus n -> str (String.make n '+') - end ++ spc()) + end) | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> |