diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/ppconstr.ml | 4 | ||||
| -rw-r--r-- | parsing/printer.ml | 10 |
2 files changed, 1 insertions, 13 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index f0a44311bc..65439dd268 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -233,10 +233,6 @@ let pr_delimited_binders kw pr_c bl = pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl | _ -> assert false -let pr_let_binder pr x a = - hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ - pr_sep_com (fun () -> brk(0,1)) (pr ltop) a) - let rec extract_prod_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_prod_binders c in diff --git a/parsing/printer.ml b/parsing/printer.ml index 4619e50ec7..dc7552fcd1 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -171,15 +171,7 @@ let pr_named_context env ne_context = ne_context ~init:(mt ())) let pr_rel_context env rel_context = - let rec prec env = function - | [] -> (mt ()) - | [b] -> str "(" ++ pr_rel_decl env b ++ str")" - | b::rest -> - let pb = pr_rel_decl env b in - let penvtl = prec (push_rel b env) rest in - str "(" ++ pb ++ str")" ++ spc () ++ penvtl - in - hov 0 (prec env (List.rev rel_context)) + pr_binders (extern_rel_context None env rel_context) let pr_rel_context_of env = pr_rel_context env (rel_context env) |