diff options
Diffstat (limited to 'ltac/tacintern.ml')
| -rw-r--r-- | ltac/tacintern.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 7cda7d1377..a72fb0d061 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -624,6 +624,8 @@ and intern_tactic_seq onlytac ist = function | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l) | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac) | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a + | TacSelect (sel, tac) -> + ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac) (* For extensions *) | TacAlias (loc,s,l) -> |