From 7628af7af9ff20d2a894673f66c3753e214623f1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 29 Dec 2017 20:20:38 +0100
Subject: [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.
---
 tactics/class_tactics.ml | 5 +++--
 tactics/tacticals.ml     | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3456d13bbe..f3581f17dd 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -693,8 +693,9 @@ module Search = struct
           let msg =
             match fst ie with
             | Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) ->
-               str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++
-                                           print_constr_env env evd y
+              str"Cannot unify " ++
+              Printer.pr_econstr_env env evd x ++ str" and " ++
+              Printer.pr_econstr_env env evd y
             | ReachedLimitEx -> str "Proof-search reached its limit."
             | NoApplicableEx -> str "Proof-search failed."
             | e -> CErrors.iprint ie
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 878e2b1f01..596feeec8b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -655,7 +655,7 @@ module New = struct
       | _ ->
 	  let name_elim =
 	    match EConstr.kind sigma elim with
-            | Const _ | Var _ -> str " " ++ print_constr_env (pf_env gl) sigma elim
+            | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
             | _ -> mt ()
 	  in
 	  user_err ~hdr:"Tacticals.general_elim_then_using"
-- 
cgit v1.2.3