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.

---
 tactics/tacintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 0bb86cbf7d..7062737382 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -106,7 +106,7 @@ let intern_hyp ist (loc,id as locid) =
   else
     Pretype_errors.error_var_not_found_loc loc id
 
-let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id)
+let intern_hyp_or_metaid ist id = intern_hyp ist id
 
 let intern_or_var ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)
-- 
cgit v1.2.3