From 0540c07354cb38bd272169ddedd5106039539569 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 25 May 2019 12:48:35 +0200
Subject: [PATCH] Relax subG mode
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

With Coq master, we otherwise fail to infer instances with subG_savedAnythingΣ, which leads to goals like

> looking for (subG
>                       (@savedAnythingΣ (@ofe_funCF val (fun _ : val => laterCF idCF))
>                          ?cFunctorContractive0) Σ)
---
 theories/base_logic/lib/iprop.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index c587e07ff..e4634323c 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -87,7 +87,7 @@ search is only triggered if the arguments of [subG] do not contain evars. Since
 instance search for [subG] is restrained, instances should persistently have [subG] as
 their first parameter to avoid loops. For example, the instances [subG_authΣ]
 and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
-Hint Mode subG + + : typeclass_instances.
+Hint Mode subG ! + : typeclass_instances.
 
 Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
 Proof.
-- 
GitLab