Commit 737efa86 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove redundant argument. Hopefully fixes compilation with Coq master.

parent 837b5190
Pipeline #13550 failed with stage
in 16 minutes and 28 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 N γ 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