From f42a673bd7bba40e63a8fd1c95bf00d8e244aee5 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Mon, 8 Aug 2016 19:12:09 +0200
Subject: [PATCH] Inhabited instance for any Empty instance.

---
 algebra/cmra.v         | 2 --
 prelude/base.v         | 2 ++
 proofmode/weakestpre.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index a388fc743..76bd0e9db 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -504,8 +504,6 @@ Section ucmra.
   Context {A : ucmraT}.
   Implicit Types x y z : A.
 
-  Global Instance ucmra_unit_inhabited : Inhabited A := populate ∅.
-
   Lemma ucmra_unit_validN n : ✓{n} (∅:A).
   Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
   Lemma ucmra_unit_leastN n x : ∅ ≼{n} x.
diff --git a/prelude/base.v b/prelude/base.v
index b046cf8e8..370621e10 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -567,6 +567,8 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 Class Empty A := empty: A.
 Notation "∅" := empty : C_scope.
 
+Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
+
 Class Top A := top : A.
 Notation "⊤" := top : C_scope.
 
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 91dd17e2c..6f0b1bb4a 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -30,7 +30,7 @@ Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
 (* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
 Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
   atomic e →
-  ElimVs (|={E1,E2}=> P) P 
+  ElimVs (|={E1,E2}=> P) P
          (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
 Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
 End weakestpre.
-- 
GitLab