diff --git a/theories/heap_lang/lib/queue.v b/theories/heap_lang/lib/queue.v index 6e2f932927eec81ac2560dc2b94e07e115f4159b..f7660f33323df7119f5aaae9693c05442144ae4c 100644 --- a/theories/heap_lang/lib/queue.v +++ b/theories/heap_lang/lib/queue.v @@ -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.