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 ----
 printing/pptactic.mli | 1 -
 2 files changed, 5 deletions(-)

(limited to 'printing')

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
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 7dbdf80aac..82cb9c0a58 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -17,7 +17,6 @@ open Pattern
 open Misctypes
 
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
 val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
 val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
 
-- 
cgit v1.2.3