diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 6ba6ebbccf53772619fa06c5b06886373ae2f679 (patch) | |
| tree | 34cde0bf35733276e41ba4bf000412bb1ee17ee5 | |
| parent | 001ae6adf5c3a926058af6a431626f4553c3f4d0 (diff) | |
Revert "Fixing printing of Arguments."
This reverts commit c90d538c8763cb90fab6071cf00236f00b3c33a2.
| -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 4056115785..d5934e1217 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1036,7 +1036,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" |