From c408cf73a6e170c7f4d3920427e4d4fdd4bef124 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Jun 2016 17:30:55 +0200
Subject: Fixing missing substitution / printing cases of TacSelect.

---
 ltac/tacsubst.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'ltac')

diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 3d8f10e008..93c5b99555 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) ->
-- 
cgit v1.2.3