From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

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

(limited to 'theories/MSets/MSetInterface.v')

diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index bd881168..74a7f6df 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