diff options
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index dcdaf9dbc1..274c3b352a 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -264,8 +264,9 @@ and subst_tacarg subst = function TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) | TacExternal (_loc,com,req,la) -> TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) - | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x + | (IntroPattern _ | TacFreshId _) as x -> x | Tacexp t -> Tacexp (subst_tactic subst t) + | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg) | TacDynamic(the_loc,t) as x -> (match Dyn.tag t with | "tactic" | "value" -> x |