diff options
| author | Pierre-Marie Pédrot | 2018-09-24 14:34:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-24 14:34:16 +0200 |
| commit | 1946a98e9f6e8cf9a619f01c406d9fc37dd56641 (patch) | |
| tree | 193f53eb55c8f88e91eb995ff3f52fce65c2bb38 /plugins/ltac/pptactic.ml | |
| parent | c6d3e0ba94ea093d1f51b374e52f49e08aa25d9a (diff) | |
| parent | 27c7b5f2eaada92897c51d974c86d148213bd475 (diff) | |
Merge PR #8499: [api] Deprecate constructors of deprecated datatypes.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4357689ee2..803d35d07c 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 @@ -507,7 +508,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 +517,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 ":" |