diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 17:30:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 17:39:23 +0200 |
| commit | c408cf73a6e170c7f4d3920427e4d4fdd4bef124 (patch) | |
| tree | 175a80dbb8c93e9c84e7a57234e1ccd7ce36e7a8 /ltac/tacsubst.ml | |
| parent | 5beb87949659ce2fb9c9e16f923c1b01bd306727 (diff) | |
Fixing missing substitution / printing cases of TacSelect.
Diffstat (limited to 'ltac/tacsubst.ml')
| -rw-r--r-- | ltac/tacsubst.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 3d8f10e00..93c5b9955 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -229,6 +229,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacSolve l -> TacSolve (List.map (subst_tactic subst) l) | TacComplete tac -> TacComplete (subst_tactic subst tac) | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a) + | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac) (* For extensions *) | TacAlias (_,s,l) -> |