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.

---
 interp/constrarg.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index d5d19f2eaa..983163ec14 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -70,4 +70,4 @@ val wit_red_expr :
 
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
 
-val wit_clause_dft_concl :  (Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
-- 
cgit v1.2.3