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.
---
 proofs/clenv.ml   | 4 ++--
 proofs/tacmach.ml | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 79b7e1599b..95e908c4dd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -575,8 +575,8 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 
 let pr_clenv clenv =
   h 0
-    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
-     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
+    (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++
+     str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++
      pr_evar_map (Some 2) clenv.evd)
 
 (****************************************************************)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 092bb5c276..182b38d350 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -127,8 +127,8 @@ open Pp
 
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
-  let penv = print_named_context env in
-  let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
+  let penv = Termops.Internal.print_named_context env in
+  let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in
   str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
-- 
cgit v1.2.3