diff options
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index c0b81e90d..ecadfca59 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -262,6 +262,7 @@ and subst_tacarg subst = function TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) | TacFreshId _ as x -> x | TacPretype c -> TacPretype (subst_glob_constr subst c) + | TacNumgoals -> TacNumgoals | Tacexp t -> Tacexp (subst_tactic subst t) | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg) | TacDynamic(the_loc,t) as x -> |