diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4357689ee2..b219ee25ca 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -28,6 +28,7 @@ open Printer open Tacexpr open Tacarg +open Tactics module Tag = struct @@ -271,6 +272,8 @@ let string_of_genarg_arg (ArgumentType arg) = in pr_sequence pr prods with Not_found -> + (* FIXME: This key, moreover printed with a low-level printer, + has no meaning user-side *) KerName.print key let pr_alias_gen pr_gen lev key l = @@ -507,7 +510,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_destruction_arg prc prlc (clear_flag,h) = pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h - let pr_inversion_kind = function + let pr_inversion_kind = let open Inv in function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" | FullInversionClear -> primitive "inversion_clear" @@ -516,7 +519,7 @@ let string_of_genarg_arg (ArgumentType arg) = if Int.equal i j then int i else int i ++ str "-" ++ int j -let pr_goal_selector toplevel = function +let pr_goal_selector toplevel = let open Goal_select in function | SelectAlreadyFocused -> str "!:" | SelectNth i -> int i ++ str ":" | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" |