From 72da3cc8c5cf607c9c461491760837de2161123e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 20 Jul 2018 18:01:18 +0200
Subject: Warnings on coercions used without being Imported

This warning makes it much easier to stop relying on `Set Automatic
Coercions Import`. Tested with success on math-classes.
---
 pretyping/classops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/classops.mli')

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index af00c0a8dc..dc193c4e74 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -113,3 +113,5 @@ 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