diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 51886c557b9bc54f7610689b22bc59597fef48c6..f51b2162fdbea8cef752f603edc56f9104cbd67b 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']