diff options
| author |  Xavier Clerc <xavier.clerc@inria.fr> | 2014-08-21 09:36:59 +0200 |
|---|---|---|
| committer | Xavier Clerc <xavier.clerc@inria.fr> | 2014-08-21 09:39:02 +0200 |
| commit | b087b121ae82e5248cdef8ef1d9efa2335a2747d (patch) | |
| tree | faceded396efc7fd310226e1298be577cc552462 /printing/ppvernac.ml | |
| parent | a0bc36b9d2c682eca18129423695372d56e8596b (diff) | |
Space after [identity] coercion keywords (beautifier).
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 4 |
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) |