From 1f796221f1304e866e48ada93d92c84f6c1d4828 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sat, 27 Oct 2018 18:59:08 +0200 Subject: [PATCH] Some missing parameters. --- theories/base_logic/bi.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v index 114d50904..3b8c338ec 100644 --- a/theories/base_logic/bi.v +++ b/theories/base_logic/bi.v @@ -144,13 +144,13 @@ Proof. exact: bupd_plainly. Qed. (** extra BI instances *) -Global Instance uPred_affine : BiAffine (uPredI M) | 0. -Proof. intros P Q. exact: pure_intro. Qed. +Global Instance uPred_affine M : BiAffine (uPredI M) | 0. +Proof. intros P. exact: pure_intro. Qed. (* Also add this to the global hint database, otherwise [eauto] won't work for many lemmas that have [BiAffine] as a premise. *) Hint Immediate uPred_affine. -Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M). +Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredSI M). Proof. exact: @plainly_exist_1. Qed. (** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *) -- GitLab