From 9b53243ca463c2f5fd958cb538b235c2909bf8b5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jan 2021 09:51:10 +0100
Subject: [PATCH] Fix typo.

---
 iris/proofmode/classes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 51886c557..f51b2162f 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -521,7 +521,7 @@ Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
            (α β : X → PROP) (mγ : X → option PROP) : PROP :=
   M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
 
-(* Typeclass for assertions around which accessors can be elliminated.
+(* Typeclass for assertions around which accessors can be eliminated.
    Inputs: [Q], [E1], [E2], [α], [β], [γ]
    Outputs: [Q']
 
-- 
GitLab