aboutsummaryrefslogtreecommitdiffhomepage
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 cfc2e48d1..547cb1de9 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1222,7 +1222,7 @@ open Decl_kinds
| Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
| [], [] -> []
| _ -> assert false in
- hov 1 (pr_sequence (fun x -> x) (aux rl cl))
+ hov 1 (pr_sequence identity (aux rl cl))
with Not_found ->
hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")