Commit 5817669e authored by Robbert Krebbers's avatar Robbert Krebbers

And more...

parent 8945d97c
Pipeline #13799 failed with stage
in 3 minutes and 18 seconds
......@@ -396,7 +396,7 @@ Definition remove_handle `{heapG Σ, queueG Σ}
Section queue_bag_spec.
Context `{!heapG Σ, !queueG Σ} (N : namespace) (Ψ : val ironProp Σ).
Global Instance is_queue_bag_uniform γ p Ψ : Uniform (is_queue_bag N γ p Ψ).
Global Instance is_queue_bag_uniform γ p : Uniform (is_queue_bag N γ p Ψ).
Proof. apply _. Qed.
Global Instance insert_handle_uniform γ q : Uniform (insert_handle γ q).
Proof. apply _. Qed.
......
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