diff options
| author | Hugo Herbelin | 2016-11-20 15:40:40 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-12-02 15:22:15 +0100 |
| commit | 00f1839a2cee1cb1fa4dc207391c4a5bb588f71a (patch) | |
| tree | 8fce5c069c8e928410d03a22c832d58f853c0f74 | |
| parent | 1c5e311d6a92deb66ba412c56516a4b71a513e01 (diff) | |
Fixing space in printing several list of implicit arguments.
| -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 be15879184..75271e21ea 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1060,7 +1060,7 @@ module Make in print_arguments nargs args ++ if not (List.is_empty more_implicits) then - str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits + prlist (fun l -> str"," ++ print_implicits l) more_implicits else (mt ()) ++ (if not (List.is_empty mods) then str" : " else str"") ++ prlist_with_sep (fun () -> str", " ++ spc()) (function |