diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v index 2eba053749d061cdbd79be1d0e506aa099e37e36..a71141f873478c5c6b31742d0b637792411b000e 100644 --- a/theories/bi/derived_laws_bi.v +++ b/theories/bi/derived_laws_bi.v @@ -1272,7 +1272,7 @@ Section persistent_bi_absorbing. End persistent_bi_absorbing. (* Affine instances *) -Global Instance emp_affine_l : Affine (PROP:=PROP) emp. +Global Instance emp_affine : Affine (PROP:=PROP) emp. Proof. by rewrite /Affine. Qed. Global Instance False_affine : Affine (PROP:=PROP) False. Proof. by rewrite /Affine False_elim. Qed.