From 2a589ada26b35c4b361e3f37adeb85705b9cf39f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 27 Oct 2016 12:46:57 +0200
Subject: [PATCH] fix compilation with Coq 8.6 (for some reason, that 'apply:'
 diverges)

---
 program_logic/own.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/program_logic/own.v b/program_logic/own.v
index e29317bb2..f23b3eb14 100644
--- a/program_logic/own.v
+++ b/program_logic/own.v
@@ -74,7 +74,7 @@ Lemma own_valid_3 γ a1 a2 a3 : own γ a1 ★ own γ a2 ★ own γ a3 ⊢ ✓ (a
 Proof. by rewrite -!own_op assoc 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