From 6e61b19d5509d06d31e5e2e1cb73dbf7d48f8d66 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Oct 2018 23:07:43 +0200
Subject: [api] Be more explicit about deprecation of debug printers.

As suggested by @mattam82
---
 engine/termops.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.mli b/engine/termops.mli
index aa0f837938..0e5d564d3f 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -341,10 +341,10 @@ val print_constr : constr -> Pp.t
 end
 
 val print_constr : constr -> Pp.t
-[@@deprecated "use Internal.print_constr_env"]
+[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"]
 
 val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
-[@@deprecated "use Internal.print_constr_env"]
+[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"]
 
 val print_rel_context : env -> Pp.t
-[@@deprecated "use Internal.print_rel_context"]
+[@@deprecated "This is an internal, debug printer. WARNING, this function is not suitable for plugin code, if you still want to use it then call [Internal.print_rel_context] instead"]
-- 
cgit v1.2.3