From 321d26480444c947ffdaaf849157fd373e40c988 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Apr 2019 10:36:21 +0200
Subject: Fix #5752: `Hint Mode` ignored for type classes that appear as
 assumptions

The creation of the local hint db now inherits the union of the modes
from the dbs passed to `typeclasses eauto`.

We could probably go further and define in a more systematic way the
metadata that should be inherited. A lot of this code could also be
cleaned-up by defining the merge of databases, so that the search code
is parametrized by just one db (the merge of the input ones).
---
 doc/sphinx/addendum/type-classes.rst | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index a5e9023732..77a6ee79cc 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -405,6 +405,8 @@ few other commands related to typeclasses.
      resolution with the local hypotheses use full conversion during
      unification.
 
+   + When considering local hypotheses, we use the union of all the modes
+     declared in the given databases.
 
    .. cmdv:: typeclasses eauto @num
 
-- 
cgit v1.2.3