aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppvernac.ml')
-rw-r--r--printing/ppvernac.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index fed4cc51c..2440a7868 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -717,12 +717,12 @@ let rec pr_vernac = function
| VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q
| VernacCoercion (_,id,c1,c2) ->
hov 1 (
- str"Coercion" ++
+ str"Coercion" ++ spc() ++
pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
| VernacIdentityCoercion (_,id,c1,c2) ->
hov 1 (
- str"Identity Coercion" ++ pr_lident id ++
+ str"Identity Coercion" ++ spc() ++ pr_lident id ++
spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
spc() ++ pr_class_rawexpr c2)