From ca6dd2805b4a00cf8425337ec1d89327c94ef397 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 13:01:36 +0200
Subject: Do not be verbose when declaring subclass hints.

There is no point in warning about eauto being the only one able to use those
hints, since they will be used by typeclass_eauto instead. It was probably an
oversight introduced quite a long time ago.
---
 tactics/class_tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 72234db688..68a78f52f9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -525,7 +525,7 @@ let make_resolve_hyp env sigma st only_classes pri decl =
              (fun (path,info,c) ->
               let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in
               make_resolves env sigma ~name:(PathHints path)
-                  (true,false,not !Flags.quiet) info ~check:true ~poly:false
+                  (true, false, false) info ~check:true ~poly:false
                  h)
                hints)
         else []
-- 
cgit v1.2.3