From f6f511e6f7928636187e93300bdf19131cdf22cc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 16 Nov 2016 13:22:45 +0100
Subject: [PATCH] use coq 8.6 mode '!' to fix diverging apply:

There are certainly more places this is useful, but let's start with this simple test
---
 theories/base_logic/derived.v | 1 +
 theories/base_logic/lib/own.v | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index b15ba0355..679db07da 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -33,6 +33,7 @@ Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
 Arguments timelessP {_} _ {_}.
 
 Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
+Hint Mode PersistentP - ! : typeclass_instances.
 Arguments persistentP {_} _ {_}.
 
 Module uPred.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 70130e826..8bc9ca71a 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -104,7 +104,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
 Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
 Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
-Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
+Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 
-- 
GitLab