diff options
| author | Pierre-Marie Pédrot | 2020-06-08 13:01:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | ca6dd2805b4a00cf8425337ec1d89327c94ef397 (patch) | |
| tree | a99d0f02917c31b03ac16c7a2b262ffe338c88ec | |
| parent | 6c4eceaa9d71df6cb608b056bebbd760b707d26e (diff) | |
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.
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 [] |