aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r--tactics/tacinterp.ml1
1 files changed, 0 insertions, 1 deletions
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)