diff options
| author | Maxime Dénès | 2018-01-23 09:59:30 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-23 09:59:30 +0100 |
| commit | 89d14fa4f16e9741108887177d43d34675261d22 (patch) | |
| tree | b2d97d58db1a1220d42639ccbd5649b1036762a7 | |
| parent | a4e4bf422093612c87bf6a55b98b8b7a7317c18a (diff) | |
| parent | e19d39cc2796345d531b5a2d7dd33980f8989bfb (diff) | |
Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and pr_lname
| -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 96e39e89a6..7e68a97e44 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 |