From f7433647beb23113faf0bf68326e5dc98e388d79 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 31 Dec 2015 17:04:07 +0100
Subject: Remove unused function Checker.print_loc.

There is no location to print anyway, so it will never be useful.
---
 checker/checker.ml | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/checker/checker.ml b/checker/checker.ml
index d5d9b9e3b8..a13d529e83 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -217,12 +217,6 @@ open Type_errors
 let anomaly_string () = str "Anomaly: "
 let report () = (str "." ++ spc () ++ str "Please report.")
 
-let print_loc loc =
-  if loc = Loc.ghost then
-    (str"<unknown>")
-  else
-    let loc = Loc.unloc loc in
-    (int (fst loc) ++ str"-" ++ int (snd loc))
 let guill s = str "\"" ++ str s ++ str "\""
 
 let where s =
-- 
cgit v1.2.3