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.

---
 intf/tacexpr.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d5a3328f02..609ee2f369 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -19,8 +19,6 @@ open Decl_kinds
 open Misctypes
 open Locus
 
-type 'a or_metaid = AI of 'a | MetaId of Loc.t * string
-
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag = bool      (* true = lazy             false = eager *)
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
-- 
cgit v1.2.3