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 +
 printing/pptactic.ml | 12 ++++++++++++
 2 files changed, 13 insertions(+)

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) ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index cfab1408bb..f8b34e2498 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -630,6 +630,17 @@ module Make
     | FullInversion -> primitive "inversion"
     | FullInversionClear -> primitive "inversion_clear"
 
+  let pr_range_selector (i, j) =
+    if Int.equal i j then int i
+    else int i ++ str "-" ++ int j
+
+  let pr_goal_selector = function
+    | SelectNth i -> int i ++ str ":"
+    | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
+        str "]" ++ str ":"
+    | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+    | SelectAll -> str "all" ++ str ":"
+
   let pr_lazy = function
     | General -> keyword "multi"
     | Select -> keyword "lazy"
@@ -1135,6 +1146,7 @@ module Make
               keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
             | TacComplete t ->
               pr_tac (lcomplete,E) t, lcomplete
+            | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
             | TacAtom (loc,t) ->
-- 
cgit v1.2.3