From d12cc91d07bc473276316474cc8f8beb9040934c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 18 Jul 2018 18:22:24 +0200
Subject: Remove `Automatic Coercions Import` option.

This option made the Coercions command follow non-standard scoping rules
(effect on `Require` rather than `Import`). It was already marked for deletion
in 8.8.
---
 pretyping/classops.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'pretyping/classops.mli')

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
-- 
cgit v1.2.3