aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--printing/ppvernac.ml2
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"