From 061e8d6a0d633381c9894cfea44f8be8a97203dd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 31 May 2018 17:18:49 +0200
Subject: [PATCH] Typo typo.

Thanks to @dfrumin.
---
 theories/base_logic/lib/boxes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 52e4d2bd1..48e7b766f 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.
-- 
GitLab