diff options
| author | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
| commit | 88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch) | |
| tree | 01f750142359361f800e0dc2dfe422f145f491c5 /interp/notation.ml | |
| parent | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff) | |
| parent | fdd6a17b272995237c9f95fc465bb1ff6871bedc (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 0b5791d32b..d18b804bfd 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -796,8 +796,8 @@ let pr_scope_classes sc = let l = classes_of_scope sc in match l with | [] -> mt () - | _ :: l -> - let opt_s = match l with [] -> mt () | _ -> str "es" in + | _ :: ll -> + let opt_s = match ll with [] -> mt () | _ -> str "es" in hov 0 (str "Bound to class" ++ opt_s ++ spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl() |