From 0736cd1ff1eb07c6faae43cdfbe2efd11c8470e9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Jul 2014 20:22:07 +0200
Subject: Removing dead code relative to or_metaid.

---
 printing/pptactic.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 90341a69b8..04e1a49232 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -82,10 +82,6 @@ let pr_or_var pr = function
   | ArgArg x -> pr x
   | ArgVar (_,s) -> pr_id s
 
-let pr_or_metaid pr = function
-  | AI x -> pr x
-  | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable"
-
 let pr_and_short_name pr (c,_) = pr c
 
 let pr_or_by_notation f = function
-- 
cgit v1.2.3