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

Fix type in lock.

parent 777e3509
No related branches found
No related tags found
No related merge requests found
...@@ -12,7 +12,7 @@ Global Opaque newlock acquire release. ...@@ -12,7 +12,7 @@ Global Opaque newlock acquire release.
(** The CMRA we need. *) (** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := SpawnG { lock_tokG :> inG heap_lang Σ (exclR unitC) }. Class lockG Σ := LockG { lock_tokG :> inG heap_lang Σ (exclR unitC) }.
Definition lockGF : gFunctorList := [GFunctor (constRF (exclR unitC))]. Definition lockGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
Instance inGF_lockG `{H : inGFs heap_lang Σ lockGF} : lockG Σ. Instance inGF_lockG `{H : inGFs heap_lang Σ lockGF} : lockG Σ.
Proof. destruct H. split. apply: inGF_inG. Qed. Proof. destruct H. split. apply: inGF_inG. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment