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

fix build

parent 43922f62
No related branches found
No related tags found
No related merge requests found
Pipeline #81833 passed
...@@ -14,7 +14,8 @@ generic mechanism for ghost state. These resources satisfy the following laws: ...@@ -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)]. Definition symbolΣ : gFunctors := #[GFunctor (authR max_natUR)].
Global Instance subG_symbolΣ {Σ} : subG symbolΣ Σ symbolG Σ. Global Instance subG_symbolΣ {Σ} : subG symbolΣ Σ symbolG Σ.
......
...@@ -14,7 +14,8 @@ following laws: ...@@ -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))]. Definition two_stateΣ : gFunctors := #[GFunctor (authR (optionUR unitR))].
Global Instance subG_two_stateΣ {Σ} : subG two_stateΣ Σ two_stateG Σ. 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