diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 52e4d2bd10607fb2ca0578374f4b4e0831086661..48e7b766f8b5605a980141eca558fb5441479482 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -14,7 +14,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.