From 9c927ebdd7e72bb4ae39b549f55f375d66683be5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 22 May 2014 00:58:56 +0200
Subject: Removing useless use of metaids in tactic AST.

---
 grammar/q_coqast.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index a52fdeb62c..cada607f67 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -83,7 +83,7 @@ let mlexpr_of_or_var f = function
   | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >>
   | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
 
-let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
+let mlexpr_of_hyp = (mlexpr_of_located mlexpr_of_ident)
 
 let mlexpr_of_occs = function
   | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >>
-- 
cgit v1.2.3