[printing] Remove duplicated printing function.

It seems there were 4 copies of the same function in the code base.

4 files changed, 6 insertions, 103 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 1db8be081..bd2ac8c67 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -22,26 +22,10 @@ open Pltac
 
 DECLARE PLUGIN "recdef_plugin"
 
-let pr_binding prc = function
-  | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
-  | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
-
-let pr_bindings prc prlc = function
-  | ImplicitBindings l ->
-      brk (1,1) ++ str "with" ++ brk (1,1) ++
-      pr_sequence prc l
-  | ExplicitBindings l ->
-      brk (1,1) ++ str "with" ++ brk (1,1) ++
-        pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
-  | NoBindings -> mt ()
-
-let pr_with_bindings prc prlc (c,bl) =
-  prc c ++ hv 0 (pr_bindings prc prlc bl)
-
 let pr_fun_ind_using  prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
-    | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b)
+    | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
 
 (* Duplication of printing functions because "'a with_bindings" is
    (internally) not uniform in 'a: indeed constr_with_bindings at the
@@ -49,17 +33,12 @@ let pr_fun_ind_using  prc prlc _ opt_c =
    "constr with_bindings"; hence, its printer cannot be polymorphic in
    (prc,prlc)... *)
 
-let pr_with_bindings_typed prc prlc (c,bl) =
-  prc c ++
-  hv 0 (pr_bindings prc prlc bl)
-
 let pr_fun_ind_using_typed prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
     | Some b ->
       let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
-      spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
-
+      spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
 
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings option
@@ -80,7 +59,6 @@ TACTIC EXTEND newfuninv
      ]
 END
 
-
 let pr_intro_as_pat _prc _ _ pat =
   match pat with
     | Some pat ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d68bdc215..bc5153253 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -26,31 +26,6 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
-(* Some pretty printing function for debugging purpose *)
-
-let pr_binding prc  =
-  function
-    | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
-    | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
-
-let pr_bindings prc prlc = function
-  | ImplicitBindings l ->
-      brk (1,1) ++ str "with" ++ brk (1,1) ++
-      pr_sequence prc l
-  | ExplicitBindings l ->
-      brk (1,1) ++ str "with" ++ brk (1,1) ++
-        pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
-  | NoBindings -> mt ()
-
-
-let pr_with_bindings prc prlc (c,bl) =
-  prc c ++ hv 0 (pr_bindings prc prlc bl)
-
-
-
-let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds =
-  pr_with_bindings prc prc  (c,bl)
-
 (* The local debugging mechanism *)
 (* let msgnl = Pp.msgnl *)
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 4e254ea76..099789061 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -161,28 +161,6 @@ type 'a extra_genarg_printer =
     | AnonHyp n -> int n
     | NamedHyp id -> pr_id id
 
-  let pr_binding prc = function
-    | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
-    | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
-
-  let pr_bindings prc prlc = function
-    | ImplicitBindings l ->
-      brk (1,1) ++ keyword "with" ++ brk (1,1) ++
-        hv 0 (prlist_with_sep spc prc l)
-    | ExplicitBindings l ->
-      brk (1,1) ++ keyword "with" ++ brk (1,1) ++
-        hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l)
-    | NoBindings -> mt ()
-
-  let pr_bindings_no_with prc prlc = function
-    | ImplicitBindings l ->
-      brk (0,1) ++
-        prlist_with_sep spc prc l
-    | ExplicitBindings l ->
-      brk (0,1) ++
-        prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
-    | NoBindings -> mt ()
-
   let pr_clear_flag clear_flag pp x =
     match clear_flag with
     | Some false -> surround (pp x)
@@ -190,7 +168,7 @@ type 'a extra_genarg_printer =
     | None -> pp x
 
   let pr_with_bindings prc prlc (c,bl) =
-    prc c ++ pr_bindings prc prlc bl
+    prc c ++ Miscprint.pr_bindings prc prlc bl
 
   let pr_with_bindings_arg prc prlc (clear_flag,c) =
     pr_clear_flag clear_flag (pr_with_bindings prc prlc) c
@@ -367,30 +345,6 @@ type 'a extra_genarg_printer =
     | EvalConstRef sp ->
       Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
 
-  let pr_esubst prc l =
-    let pr_qhyp = function
-    (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
-      | (_,(NamedHyp id,c)) ->
-        str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
-    in
-    prlist_with_sep spc pr_qhyp l
-
-  let pr_bindings_gen for_ex prc prlc = function
-    | ImplicitBindings l ->
-      spc () ++
-        hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
-                 prlist_with_sep spc prc l)
-    | ExplicitBindings l ->
-      spc () ++
-        hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
-                 pr_esubst prlc l)
-    | NoBindings -> mt ()
-
-  let pr_bindings prc prlc = pr_bindings_gen false prc prlc
-
-  let pr_with_bindings prc prlc (c,bl) =
-    hov 1 (prc c ++ pr_bindings prc prlc bl)
-
   let pr_as_disjunctive_ipat prc ipatl =
     keyword "as" ++ spc () ++
       pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
@@ -1280,9 +1234,9 @@ let () =
     (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
   Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
   Genprint.register_print0 wit_bindings
-    (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
-    (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it)));
+    (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
+    (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it)));
   Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 19bdf2d49..4265c416b 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -106,10 +106,6 @@ val pr_hintbases : string list option -> std_ppcmds
 
 val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
 
-val pr_bindings :
-  ('constr -> std_ppcmds) ->
-  ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
-
 val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
 
 val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->