diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 15:27:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 15:27:09 +0200 |
| commit | 01050348ca54a3ac42da954d85b19c331d0c11db (patch) | |
| tree | 025286c27b970d1f548785640b362b7ced08d0fb /plugins/ltac/pptactic.ml | |
| parent | 3af594bb07b3faf8d766bb1e9b6bead7cb1081d8 (diff) | |
| parent | c0b244260badedf27fe2b66d3c058ad681af4371 (diff) | |
Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 8a0764975..d8bd16620 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -477,12 +477,14 @@ type 'a extra_genarg_printer = 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 "[" ++ Id.print id ++ str "]" ++ str ":" - | SelectAll -> str "all" ++ str ":" +let pr_goal_selector toplevel = function + | SelectNth i -> int i ++ str ":" + | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" + | SelectId id -> str "[" ++ Id.print id ++ str "]:" + | SelectAll -> assert toplevel; str "all:" + +let pr_goal_selector ~toplevel s = + (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s let pr_lazy = function | General -> keyword "multi" @@ -988,7 +990,7 @@ type 'a extra_genarg_printer = 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 + | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false 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) -> |