From c568ece0b549f26d48fc961cd80e2f0e0af46969 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 16:32:22 +0100
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)

---
 docs/equalities_and_entailments.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/equalities_and_entailments.md b/docs/equalities_and_entailments.md
index 201f0db9f..55be1f0c4 100644
--- a/docs/equalities_and_entailments.md
+++ b/docs/equalities_and_entailments.md
@@ -7,7 +7,7 @@ This is not a general introduction to Iris: instead, we discuss the different
 Iris equalities and the interface to their Coq implementation. In particular, we
 discuss:
 - Equality ("=") in the *on-paper* Iris metatheory
-- Coq equality (`=`) and setoid equivalence (`≡`);
+- Coq's Leibniz equality (`=`) and std++'s setoid equivalence (`≡`);
 - N-equivalence on OFEs (`≡{n}≡`);
 - Iris internal equality (`≡` in `bi_scope`);
 - Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
@@ -122,7 +122,7 @@ a Coq-level statement of type `Prop`, the latter an Iris-level statement of type
 `iProp`.  However, the two are closely related: `P ⊢ Q` is equivalent to `emp ⊢
 P -∗ Q` (per Iris lemmas `entails_wand` and `wand_entails`).  Iris also defines
 a "unary" form of entailment, `⊢ P`, which is short for `emp ⊢ P`.
-We can also use bi-entailment `P ⊣⊢ Q` to express that both `P ⊢ Q` and `Q ⊢ P` gold.
+We can also use bi-entailment `P ⊣⊢ Q` to express that both `P ⊢ Q` and `Q ⊢ P` hold.
 
 On paper, uniform predicates are defined by quotienting by an equivalence
 relation ([Iris appendix, Sec. 3.3]); in Coq, that relation is chosen as the
-- 
GitLab