From d927b406f7ce3bd147de00510b1aee9cc6c3705f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 19 Dec 2017 17:23:18 +0100
Subject: [PATCH] Fix Hint Mode.

---
 theories/proofmode/monpred.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index f3842e4b8..c6f43bfd0 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -6,7 +6,7 @@ Class MakeMonPredCar {I : bi_index} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
   make_monPred_car : P i ⊣⊢ 𝓟.
 Arguments MakeMonPredCar {_ _} _ _%I _%I.
-Hint Mode MakeMonPredCar + + - ! -.
+Hint Mode MakeMonPredCar + + - ! - : typeclass_instances.
 
 Section bi.
 Context {I : bi_index} {PROP : bi}.
-- 
GitLab