diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 80199a06f0721afec817cafad4464b732107d83d..a7d42b450cf0b293ee2027b18bff9c8d2b9c9afb 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -408,10 +408,10 @@ search, and do not carry any information: [FrameNoInstantiateExist] is
 equivalent to [True], but does not come with any instances.
 Recursive [Frame] instances can disable instantiating existentials in their
 recursive search by replacing the recursive [Frame ...] premise with
-[FrameNoInstantiateExist → Frame ...]. This explicitly adds a
+[(FrameNoInstantiateExist → Frame ...)]. This explicitly adds a
 [FrameNoInstantiateExist] hypothesis to the recursive [Frame] search,
 causing [FrameNoInstantiateExist] to have instances in that recursive search.
-This will disables the instance that instantiates existential quantifiers. *)
+This will disable the instance that instantiates existential quantifiers. *)
 Class FrameNoInstantiateExist : Prop := frame_no_instantiate_exist : True.
 (* We disable that instance by adding a new premise to it: an instance of the
 [FrameCanInstantiateExist] type class, defined using stdpp's [TCUnless]. *)