aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli3
1 files changed, 2 insertions, 1 deletions
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