Make envs_entails opaque.

957d5fcf · Jacques-Henri Jourdan · b2426163 · 957d5fcf
Commit 957d5fcf authored Feb 13, 2018 by Jacques-Henri Jourdan
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

theories/proofmode/coq_tactics.v theories/proofmode/coq_tactics.v +4 -0

No files found.
--- 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.