diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 7fad6fb9ab..1866ca5042 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -85,8 +85,8 @@ end) = struct mt () | UnpMetaVar (_, prec) as unp :: l -> let c = pop env in - let pp1= pr (n, prec) c in let pp2 = aux l in + let pp1 = pr (n, prec) c in return unp pp1 pp2 | UnpListMetaVar (_, prec, sl) as unp :: l -> let cl = pop envlist in @@ -95,16 +95,15 @@ end) = struct return unp pp1 pp2 | UnpBinderListMetaVar (_, isopen, sl) as unp :: l -> let cl = pop bll in - let pp1 = pr_binders (fun () -> aux sl) isopen cl in let pp2 = aux l in + let pp1 = pr_binders (fun () -> aux sl) isopen cl in return unp pp1 pp2 | UnpTerminal s as unp :: l -> - let pp1 = str s in let pp2 = aux l in + let pp1 = str s in return unp pp1 pp2 | UnpBox (b,sub) as unp :: l -> - let pp1 = aux sub in - let pp1 = ppcmd_of_box b pp1 in + let pp1 = ppcmd_of_box b (aux sub) in let pp2 = aux l in return unp pp1 pp2 | UnpCut cut as unp :: l -> @@ -115,12 +114,8 @@ end) = struct aux unps let pr_notation pr pr_binders s env = - let unpl, level, trailing_level = find_notation_printing_rule s in - let pp = print_hunks level pr pr_binders env unpl in - let level = match trailing_level with - | Some (level',_) -> max level level' - | _ -> level in - pp, level + let unpl, level = find_notation_printing_rule s in + print_hunks level pr pr_binders env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) |