diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-26 14:34:51 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-26 14:37:28 +0200 |
| commit | c0b244260badedf27fe2b66d3c058ad681af4371 (patch) | |
| tree | 42d2167549e386e1a809b59f9059e10322a88805 /plugins/ltac/g_ltac.ml4 | |
| parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
Properly display the "only" prefix for selectors (bug #5760).
This commit also fixes range selectors being incorrectly displayed.
Diffstat (limited to 'plugins/ltac/g_ltac.ml4')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 2ea0f60eb..86c983bdd 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -388,16 +388,7 @@ let vernac_solve n info tcom b = p,status) in if not status then Feedback.feedback Feedback.AddedAxiom -let pr_range_selector (i, j) = - if Int.equal i j then int i - else int i ++ str "-" ++ int j - -let pr_ltac_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_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector | [ toplevel_selector(s) ] -> [ s ] |