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.

---
 intf/tacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d03279fc3f..01e01ff858 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -258,7 +258,7 @@ type r_pat = constr_pattern_expr
 type r_cst = reference or_by_notation
 type r_ind = reference or_by_notation
 type r_ref = reference
-type r_nam  = Id.t located or_metaid
+type r_nam  = Id.t located
 type r_lev = rlevel
 
 type raw_atomic_tactic_expr =
-- 
cgit v1.2.3