From e19d39cc2796345d531b5a2d7dd33980f8989bfb Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 22 Jan 2018 08:31:17 +0000 Subject: [printing] Remove duplicate definitions of pr_lident and pr_lname --- printing/ppvernac.ml | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 96e39e89a..7e68a97e4 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -31,12 +31,6 @@ open Decl_kinds let pr_lconstr = pr_lconstr_expr let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr - let pr_lident (loc,id) = - match loc with - | None -> pr_id id - | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id - let pr_uconstraint (l, d, r) = pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_glob_level r @@ -77,10 +71,6 @@ open Decl_kinds | Some loc -> let (b,_) = Loc.unloc loc in pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid - let pr_lname = function - | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located Name.print lna - let pr_smart_global = Pputils.pr_or_by_notation pr_reference let pr_ltac_ref = Libnames.pr_reference -- cgit v1.2.3