From d4a421e57d74d305a797897f43ce216fb4c39719 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 14 Mar 2016 11:16:19 +0100
Subject: Typeclasses: stdlib fixes for new search algorithm

---
 theories/MSets/MSetInterface.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'theories/MSets')

diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index bd8811689..74a7f6df8 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -345,6 +345,9 @@ Module Type WRawSets (E : DecidableType).
       predicate [Ok]. If [Ok] isn't decidable, [isok] may be the
       always-false function. *)
   Parameter isok : t -> bool.
+  (** MS: 
+    Dangerous instance, the [isok s = true] hypothesis cannot be discharged
+   with typeclass resolution. Is it really an instance? *)
   Declare Instance isok_Ok s `(isok s = true) : Ok s | 10.
 
   (** Logical predicates *)
-- 
cgit v1.2.3