Skip to content
Snippets Groups Projects
Commit 43922f62 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix 8.16 build

parent a66e4add
No related branches found
No related tags found
No related merge requests found
Pipeline #81831 failed
......@@ -14,7 +14,8 @@ generic mechanism for ghost state. These resources satisfy the following laws:
>>
*)
Class symbolG Σ := { symbol_inG :: inG Σ (authR max_natUR) }.
Class symbolG Σ := { symbol_inG : inG Σ (authR max_natUR) }.
Local Existing Instance symbol_inG.
Definition symbolΣ : gFunctors := #[GFunctor (authR max_natUR)].
Global Instance subG_symbolΣ {Σ} : subG symbolΣ Σ symbolG Σ.
......
......@@ -14,7 +14,8 @@ following laws:
>>
*)
Class two_stateG Σ := { two_state_inG :: inG Σ (authR (optionUR unitR)) }.
Class two_stateG Σ := { two_state_inG : inG Σ (authR (optionUR unitR)) }.
Local Existing Instance two_state_inG.
Definition two_stateΣ : gFunctors := #[GFunctor (authR (optionUR unitR))].
Global Instance subG_two_stateΣ {Σ} : subG two_stateΣ Σ two_stateG Σ.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment