Skip to content
Snippets Groups Projects
Commit 061e8d6a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Typo typo. 

Thanks to @dfrumin.
parent ad0201e9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/boxes.v
+ 1
− 1
View file @ 061e8d6a
...@@ -14,7 +14,7 @@ Class boxG Σ := ...@@ -14,7 +14,7 @@ Class boxG Σ :=
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) * Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
optionRF (agreeRF (▶ ∙)) ) ]. optionRF (agreeRF (▶ ∙)) ) ].
Instance subG_stsΣ Σ : subG boxΣ Σ → boxG Σ. Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Section box_defs. Section box_defs.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment