From bf9fd4f5bb4f524cb3c0c3437c33e4af863c6620 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jun 2018 15:33:45 +0200
Subject: [PATCH] allow FrameMonPredAt to infer the index

---
 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 68920fb9a..68ac02005 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -21,7 +21,7 @@ Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
       (𝓡 : PROP) (P : monPred I PROP) (𝓠 : PROP) :=
   frame_monPred_at : □?p 𝓡 ∗ 𝓠 -∗ P i.
 Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
-Hint Mode FrameMonPredAt + + + + ! ! - : typeclass_instances.
+Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
 
 Section modalities.
   Context {I : biIndex} {PROP : bi}.
-- 
GitLab