From 00f11e6869b8f3964e6c3ecad5b67800b6853ed7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Apr 2003 12:08:38 +0000
Subject: Bug: lookup inapproprie dans subst_tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3921 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index efeacafe81..514557d349 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1931,7 +1931,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 
   (* For extensions *)
   | TacExtend (_loc,opn,l) ->
-      let _ = lookup_tactic opn in
       TacExtend (loc,opn,List.map (subst_genarg subst) l)
   | TacAlias (s,l,body) ->
       TacAlias (s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,subst_tactic subst body)
-- 
cgit v1.2.3