diff options
| author | Pierre-Marie Pédrot | 2016-06-16 17:30:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-16 17:39:23 +0200 |
| commit | c408cf73a6e170c7f4d3920427e4d4fdd4bef124 (patch) | |
| tree | 175a80dbb8c93e9c84e7a57234e1ccd7ce36e7a8 | |
| parent | 5beb87949659ce2fb9c9e16f923c1b01bd306727 (diff) | |
Fixing missing substitution / printing cases of TacSelect.
| -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) -> |