aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppvernac.ml
diff options
context:
space:
mode:
authorGravatar Xavier Clerc <xavier.clerc@inria.fr>2014-08-21 09:37:40 +0200
committerGravatar Xavier Clerc <xavier.clerc@inria.fr>2014-08-21 09:39:02 +0200
commit8ef5bfc24e15a80153f03c1efe88448c1169bdd0 (patch)
tree3aab32b112f1fec0542b36e8212e25f8510ae66f /printing/ppvernac.ml
parent9c390adab04228d326b30b662ab82f3f3cdf4b8f (diff)
Improve consistency of whitespace (beautifier).
Diffstat (limited to 'printing/ppvernac.ml')
-rw-r--r--printing/ppvernac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 17b61f30f..dce073bec 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -775,7 +775,7 @@ let rec pr_vernac = function
prlist_with_sep (fun () -> str " <+ ") pr_mt m)
| VernacInclude (mexprs) ->
let pr_m = pr_module_ast_inl false pr_lconstr in
- hov 2 (str"Include " ++
+ hov 2 (str"Include" ++ spc() ++
prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
(* Solving *)
| VernacSolve (i,tac,deftac) ->