diff options
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index deac1d4ff..ba37c1019 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -247,6 +247,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacTry tac -> TacTry (subst_tactic subst tac) | TacInfo tac -> TacInfo (subst_tactic subst tac) | TacRepeat tac -> TacRepeat (subst_tactic subst tac) + | TacOr (tac1,tac2) -> + TacOr (subst_tactic subst tac1,subst_tactic subst tac2) | TacOrelse (tac1,tac2) -> TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2) | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) |