diff options
| author | Maxime Dénès | 2017-04-24 14:45:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-24 14:45:53 +0200 |
| commit | 4c92188d485cf5d27c9a73caf2be8c149cb4f883 (patch) | |
| tree | c47688b392359e58493c6dac8ce85bcb4e9c5789 /printing | |
| parent | b57ff91ae70cb8bb086499fad07aa40b39cb8de2 (diff) | |
| parent | 40f7eb94b653b60f79c4f6eb204960037fcffa66 (diff) | |
Merge PR#552: Miscelaneous commits
Diffstat (limited to 'printing')
| -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 5af0e1d9b3..e4a87739b1 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1221,7 +1221,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 ")") |