From 957d5fcfd62239a2e561ed0335bec65e36483a1a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 13 Feb 2018 14:41:29 +0100
Subject: [PATCH] Make envs_entails opaque.

---
 theories/proofmode/coq_tactics.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index ca5e4f6c3..35d576c93 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1249,3 +1249,7 @@ Proof.
   by rewrite affinely_persistently_sep_2 wand_elim_r affinely_elim.
 Qed.
 End sbi_tactics.
+
+(* We make [envs_entails] opaque, so that it does not get unfolded by
+   the proofmode's own tactics, such as [iIntros (?)]. *)
+Opaque envs_entails.
-- 
GitLab