diff --git a/ProofMode.md b/ProofMode.md
index cb1ef692fca46f85d94bb9c94475004e75b23a12..4fb2039588578bd6d916357d324d55f103313bc4 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -41,7 +41,7 @@ Context management
   the resulting goal.
 - `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
   eliminates it. This tactic is essentially the same as `iDestruct` with the
-  difference that when `pm_trm` is a non-universally quantified spatial
+  difference that when `pm_trm` is a non-universally quantified intuitionistic
   hypothesis, it will not throw the hypothesis away.
 - `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
   hypothesis `P` to the current goal. The specialization pattern `spat`
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index ea423840b7c4684009a23e86d7302e77d094781e..597f175ab0b6ee5cf9ecbe70cc04bdf89ed9f830 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -13,7 +13,7 @@ Class boxG Σ :=
 Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
                                             optionRF (agreeRF (▶ ∙)) ) ].
 
-Instance subG_stsΣ Σ : subG boxΣ Σ → boxG Σ.
+Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
 Proof. solve_inG. Qed.
 
 Section box_defs.