aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-01-22 08:31:17 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-01-22 08:31:17 +0000
commite19d39cc2796345d531b5a2d7dd33980f8989bfb (patch)
tree39eb7137f514211bfccd30bb3e65a352bf72bbbd
parent9aa2464375c1515aa64df7dc910e2f324e34c82f (diff)
[printing] Remove duplicate definitions of pr_lident and pr_lname
-rw-r--r--printing/ppvernac.ml10
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