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/pretyping.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a4c2cb2352..b9345190fb 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -976,9 +976,9 @@ and pretype_instance k0 resolve_tc env evdref loc hyps evk update =
              pr_existential_key !evdref evk ++
              strbrk " in current context: binding for " ++ Id.print id ++
              strbrk " is not convertible to its expected definition (cannot unify " ++
-             quote (print_constr_env !!env !evdref b) ++
+             quote (Termops.Internal.print_constr_env !!env !evdref b) ++
              strbrk " and " ++
-             quote (print_constr_env !!env !evdref c) ++
+             quote (Termops.Internal.print_constr_env !!env !evdref c) ++
              str ").")
       | Some b, None ->
            user_err ?loc  (str "Cannot interpret " ++
-- 
cgit v1.2.3