Commit 8945d97c authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of more redundant arguments.

parent 737efa86
Pipeline #13551 failed with stage
in 16 minutes and 20 seconds
......@@ -188,11 +188,11 @@ Section queue_spec.
Uniform (queue_inv γ lhptr ltptr).
Proof. repeat (apply exist_uniform=> ?); case_match; apply _. Qed.
Global Instance is_queue_persistent N γ q : Persistent (is_queue N γ q).
Global Instance is_queue_persistent γ q : Persistent (is_queue N γ q).
Proof. apply _. Qed.
Global Instance is_queue_affine N γ q : Affine (is_queue N γ q).
Global Instance is_queue_affine γ q : Affine (is_queue N γ q).
Proof. apply _. Qed.
Global Instance is_queue_uniform N γ q : Uniform (is_queue N γ q).
Global Instance is_queue_uniform γ q : Uniform (is_queue N γ q).
Proof. apply affine_uniform, _. Qed.
Global Instance enqueue_handle_uniform γ q : Uniform (enqueue_handle γ q).
......
Markdown is supported
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