From f2437bb0f10e3945ae263e31f44849b646102b5f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 9 Nov 2019 11:07:35 +0100
Subject: [PATCH] More relaxed mode for `MakeMonPredAt`.

This is needed to fix RustBelt-related. Since type classes are no longer
over-eagerly resolved, the `biIndex` now sometimes contains an evar.
---
 theories/proofmode/monpred.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 97df3d632..eca1b6094 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -6,7 +6,10 @@ Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
   make_monPred_at : P i ⊣⊢ 𝓟.
 Arguments MakeMonPredAt {_ _} _ _%I _%I.
-Hint Mode MakeMonPredAt + + - ! - : typeclass_instances.
+(** Since [MakeMonPredAt] is used by [AsEmpValid] to import lemmas into the
+proof mode, the index [I] and BI [PROP] often contain evars. Hence, it is
+important to use the mode [!] also for the first two arguments. *)
+Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
 
 Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i ⊑ j.
 Hint Mode IsBiIndexRel + - - : typeclass_instances.
-- 
GitLab