From 23fcb09d934bf77fe58f232d2c246a81fc76591f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 16 Nov 2018 13:24:54 +0000
Subject: [Typeclasses] Warn when RHS of `:>` is not a class

This introduces the warning “not-a-class” in the “typeclasses” category.
---
 pretyping/typeclasses.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.mli')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 8bdac0a575..d00195678b 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -133,7 +133,10 @@ val remove_instance_hint : GlobRef.t -> unit
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-val declare_instance : hint_info option -> bool -> GlobRef.t -> unit
+(** Declares the given global reference as an instance of its type.
+    Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
+    when said type is not a registered type class. *)
+val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
-- 
cgit v1.2.3