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.

---
 grammar/q_coqast.ml4 | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'grammar')

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 360b96dc4a..d1f4587915 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -71,10 +71,6 @@ let mlexpr_of_intro_pattern = function
 
 let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
 
-let mlexpr_of_or_metaid f = function
-  | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >>
-  | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >>
-
 let mlexpr_of_quantified_hypothesis = function
   | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >>
   | Misctypes.NamedHyp id ->  <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >>
-- 
cgit v1.2.3