From 737efa86cdc1d81e39bb795e093cb5d9129a4d84 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Mon, 24 Dec 2018 11:21:58 +0100 Subject: [PATCH] Remove redundant argument. Hopefully fixes compilation with Coq master. --- theories/heap_lang/lib/queue.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/heap_lang/lib/queue.v b/theories/heap_lang/lib/queue.v index 6e2f932..f7660f3 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. -- GitLab