diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacsubst.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 3d8f10e008..93c5b99555 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -229,6 +229,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacSolve l -> TacSolve (List.map (subst_tactic subst) l) | TacComplete tac -> TacComplete (subst_tactic subst tac) | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a) + | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac) (* For extensions *) | TacAlias (_,s,l) -> |