From 58f891c100d1a1821ed6385c1d06f9e0a77ecdac Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 6 Nov 2018 09:30:45 +0100
Subject: Move debug term printer to kernel

---
 engine/termops.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 07c9541f25..6c3d4fa612 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -17,9 +17,10 @@ open Environ
 open EConstr
 
 (** printers *)
-val print_sort : Sorts.t -> Pp.t
 val pr_sort_family : Sorts.family -> Pp.t
+[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
 val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
+[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
 
 (** about contexts *)
 val push_rel_assum : Name.t * types -> env -> env
-- 
cgit v1.2.3