From 913ccc7fb4a987ddd7c591d3c7d75579dc502a95 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Dec 2018 08:07:32 +0100
Subject: [api] Move reduction modules to `tactics`

These modules do actually belong there.

We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
---
 plugins/ltac/pptactic.ml | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 55e58187b0..8bf1855fe0 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) =
-- 
cgit v1.2.3