aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.mli')
-rw-r--r--pretyping/classops.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 7c4842c8ae..ed2c5478f0 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -113,5 +113,3 @@ val coercions : unit -> coe_info_typ list
(** [hide_coercion] returns the number of params to skip if the coercion must
be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
val hide_coercion : coe_typ -> int option
-
-val is_coercion_in_scope : GlobRef.t -> bool