From 16294edf70bb373bb38fa3a7d271523f5402c1c6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Wed, 24 Mar 2021 01:39:17 +0100
Subject: [PATCH] Fix for Coq PR#13952

---
 src/lib/hhutils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lib/hhutils.ml b/src/lib/hhutils.ml
index e5d886dd..c52f43a4 100644
--- a/src/lib/hhutils.ml
+++ b/src/lib/hhutils.ml
@@ -670,7 +670,7 @@ let find_hints db secvars env evd t =
     let hints =
       if Termops.occur_existential evd t then
         match Hint_db.map_existential evd ~secvars hdc t db with
-        | ModeMatch l -> l
+        | ModeMatch (m, l) -> l
         | ModeMismatch -> []
       else
         Hint_db.map_auto env evd ~secvars hdc t db