diff options
-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 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 ")") |