From 80e3bc3116673c314c70adc3852099c21dd492c7 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sun, 13 May 2018 21:35:18 +0200 Subject: [PATCH] Fix typo. --- theories/bi/derived_laws_bi.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v index 2eba05374..a71141f87 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. -- GitLab