diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 2f41ff2aea..42ea649ecd 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -691,6 +691,8 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacOnce tac -> ist.ltacvars, TacOnce (intern_pure_tactic ist tac) + | TacExactlyOnce tac -> + ist.ltacvars, TacExactlyOnce (intern_pure_tactic ist tac) | TacOrelse (tac1,tac2) -> ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l) |