diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-22 08:31:17 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-22 08:31:17 +0000 |
| commit | e19d39cc2796345d531b5a2d7dd33980f8989bfb (patch) | |
| tree | 39eb7137f514211bfccd30bb3e65a352bf72bbbd /printing | |
| parent | 9aa2464375c1515aa64df7dc910e2f324e34c82f (diff) | |
[printing] Remove duplicate definitions of pr_lident and pr_lname
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 0 insertions, 10 deletions
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 |