diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2017-04-14 14:44:04 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-04-20 13:11:50 +0200 |
| commit | d13eb9c5ab01080a12e3bcb5cc54159ec365bee4 (patch) | |
| tree | 1ee6079032e567b879f89f1340ff45dde4726a5e /printing/ppvernac.ml | |
| parent | aaf20df2f9e531f1f05fbf72de796f9761cd646b (diff) | |
refactoring "Ppvernac.pr_extend"
Diffstat (limited to 'printing/ppvernac.ml')
| -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 ")") |