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 44327abef2..7c968865ac 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -251,6 +251,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with TacOr (subst_tactic subst tac1,subst_tactic subst tac2) | TacOnce tac -> TacOnce (subst_tactic subst tac) + | TacExactlyOnce tac -> + TacExactlyOnce (subst_tactic subst tac) | TacOrelse (tac1,tac2) -> TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2) | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) |