Skip to content

GitLab

Commit 1f796221 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Some missing parameters.

parent 625d60c3
Hide whitespace changes
Inline Side-by-side
Showing with 3 additions and 3 deletions
theories/base_logic/bi.v
View file @ 1f796221
......@@ -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) *)
......
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