From af46368a7595994e58ddd4cf0e06706d12bf2d37 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Mon, 29 Jun 2020 15:23:08 +0200
Subject: [PATCH] Use apply with explicit hole

---
 theories/proofmode/ltac_tactics.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 8709d8e26..bfee52173 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -3246,17 +3246,17 @@ below; see the discussion in !75 for further details. *)
 Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
   rewrite envs_entails_eq; apply internal_eq_refl : core.
 Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
-  rewrite envs_entails_eq; apply: big_sepL_nil' : core.
+  rewrite envs_entails_eq; apply (big_sepL_nil' _) : core.
 Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
-  rewrite envs_entails_eq; apply: big_sepL2_nil' : core.
+  rewrite envs_entails_eq; apply (big_sepL2_nil' _) : core.
 Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
-  rewrite envs_entails_eq; apply: big_sepM_empty' : core.
+  rewrite envs_entails_eq; apply (big_sepM_empty' _) : core.
 Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
-  rewrite envs_entails_eq; apply: big_sepM2_empty' : core.
+  rewrite envs_entails_eq; apply (big_sepM2_empty' _) : core.
 Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
-  rewrite envs_entails_eq; apply: big_sepS_empty' : core.
+  rewrite envs_entails_eq; apply (big_sepS_empty' _) : core.
 Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
-  rewrite envs_entails_eq; apply: big_sepMS_empty' : core.
+  rewrite envs_entails_eq; apply (big_sepMS_empty' _) : core.
 
 (* These introduce as much as possible at once, for better performance. *)
 Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros : core.
-- 
GitLab