diff options
| author | Hugo Herbelin | 2016-04-13 00:34:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:43:27 +0200 |
| commit | 99a7a6d28d1eda5ddcce4855cce1cf381fe21f33 (patch) | |
| tree | 1d7ef5aa222af80e28ad1996258d34c31a6bf629 | |
| parent | d28f2685615450c3c807764ce12bfdbe62450a01 (diff) | |
Fixing printing of 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 999d257486..28f6f3f3f9 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1032,7 +1032,7 @@ module Make spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ aux (n-1) tl in prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ - if not (List.is_empty mods) then str" : " else str"" ++ + (if not (List.is_empty mods) then str" : " else str"") ++ prlist_with_sep (fun () -> str", " ++ spc()) (function | `ReductionDontExposeCase -> keyword "simpl nomatch" | `ReductionNeverUnfold -> keyword "simpl never" |