aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli5
1 files changed, 3 insertions, 2 deletions
diff --git a/engine/termops.mli b/engine/termops.mli
index 1054fbbc5e..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
@@ -282,7 +283,7 @@ val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
val isGlobalRef : Evd.evar_map -> constr -> bool
-val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool
+val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool
val is_Prop : Evd.evar_map -> constr -> bool
val is_Set : Evd.evar_map -> constr -> bool