Typo

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]. *)