diff options
| author | Pierre-Marie Pédrot | 2018-12-17 18:10:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-17 18:10:03 +0100 |
| commit | dff69611da6ac1ea0e61228ede3cc8e320fcd914 (patch) | |
| tree | 1486cac06f945a758eae56bdb7e7d4c8be5a7a14 /plugins/ltac/pptactic.ml | |
| parent | 28c7600cdc56ce7dfdabe058db57883a73653298 (diff) | |
| parent | 1d0e7063fe10fbf27a1b0a8296c69ed6b661d70e (diff) | |
Merge PR #9153: [api] Move reduction modules to `tactics`
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 2267d43d93..5e3f4df192 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -22,8 +22,8 @@ open Tactypes open Locus open Decl_kinds open Genredexpr -open Pputils open Ppconstr +open Pputils open Printer open Genintern @@ -159,8 +159,8 @@ let string_of_genarg_arg (ArgumentType arg) = end | _ -> default - let pr_with_occurrences pr c = pr_with_occurrences pr keyword c - let pr_red_expr pr c = pr_red_expr pr keyword c + let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c + let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> @@ -186,12 +186,6 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c - let pr_or_by_notation f = CAst.with_val (function - | AN v -> f v - | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) - - let pr_located pr (_,x) = pr x - let pr_evaluable_reference = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) @@ -694,7 +688,7 @@ let pr_goal_selector ~toplevel s = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = |