[print] Restrict use of "debug" Termops printer.

The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.

We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.

2 files changed, 13 insertions, 10 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index ce620d5312..f26ec0f401 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -26,6 +26,10 @@ let init_size=5
 
 let cc_verbose=ref false
 
+let print_constr t =
+  let sigma, env = Pfedit.get_current_context () in
+  Printer.pr_econstr_env env sigma t
+
 let debug x =
   if !cc_verbose then Feedback.msg_debug (x ())
 
@@ -483,10 +487,10 @@ let rec inst_pattern subst = function
 	   args t
 
 let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
+  print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
 
 let pr_term t = str "[" ++
-  Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
+  print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
 
 let rec add_term state t=
   let uf=state.uf in
@@ -601,7 +605,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
+                  (str "  [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
@@ -609,7 +613,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
+                  (str "  [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 48d677a864..6bab8d0353 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Pp
 open Tacexpr
-open Termops
 
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
@@ -51,8 +50,8 @@ let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
 let db_pr_goal gl =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
-  let penv = print_named_context env in
-  let pc = print_constr_env env (Tacmach.New.project gl) concl in
+  let penv = Termops.Internal.print_named_context env in
+  let pc = Printer.pr_econstr_env env (Tacmach.New.project gl) concl in
     str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
@@ -243,7 +242,7 @@ let db_constr debug env sigma c =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c)
+    msg_tac_debug (str "Evaluated term: " ++ Printer.pr_econstr_env env sigma c)
   else return ()
 
 (* Prints the pattern rule *)
@@ -268,7 +267,7 @@ let db_matched_hyp debug env sigma (id,_,c) ido =
   is_debug debug >>= fun db ->
   if db then
     msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++
-                str " has been matched: " ++ print_constr_env env sigma c)
+                str " has been matched: " ++ Printer.pr_econstr_env env sigma c)
   else return ()
 
 (* Prints the matched conclusion *)
@@ -276,7 +275,7 @@ let db_matched_concl debug env sigma c =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c)
+    msg_tac_debug (str "Conclusion has been matched: " ++ Printer.pr_econstr_env env sigma c)
   else return ()
 
 (* Prints a success message when the goal has been matched *)