diff options
| -rw-r--r-- | ltac/tacsubst.ml | 1 | ||||
| -rw-r--r-- | printing/pptactic.ml | 12 |
2 files changed, 13 insertions, 0 deletions
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) -> |