From cedb9df534cb4b43e9c7642901567f7087e2e1fa Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 27 Jun 2021 13:11:38 +0200
Subject: [PATCH] Make sum_inhabited_r not a copy of sum_inhabited_l
This existed at least as far back as
iris/stdpp@361308c7b173f353afd99499e8bfcf168fdab1ca, 8 years ago.
---
theories/base.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index 2de46541..31f5a474 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -749,8 +749,8 @@ Global Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
Global Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
match iA with populate x => populate (inl x) end.
-Global Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
- match iB with populate y => populate (inl y) end.
+Global Instance sum_inhabited_r {A B} (iB : Inhabited B) : Inhabited (A + B) :=
+ match iB with populate y => populate (inr y) end.
Global Instance inl_inj {A B} : Inj (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
--
GitLab