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.
---
 pretyping/globEnv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/globEnv.ml')

diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 25510826cc..63a66b471b 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -140,7 +140,7 @@ let protected_get_type_of env sigma c =
   try Retyping.get_type_of ~lax:true env sigma c
   with Retyping.RetypeError _ ->
     user_err
-      (str "Cannot reinterpret " ++ quote (print_constr c) ++
+      (str "Cannot reinterpret " ++ quote (Termops.Internal.print_constr_env env sigma c) ++
        str " in the current environment.")
 
 let invert_ltac_bound_name env id0 id =
-- 
cgit v1.2.3