From ccd9cdacc45168e976a1c971cd6deda61d51b783 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 26 Feb 2024 18:04:32 +0100
Subject: [PATCH] Typo

---
 iris/proofmode/classes.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 80199a06f..a7d42b450 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]. *)
-- 
GitLab