From c136a4404e270c700c4aa93f5e882000c5cd48cf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 27 Nov 2017 16:53:16 +0100
Subject: [PATCH] No longer let `to_agree` require the carrier to be an OFE.

---
 theories/algebra/agree.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 78c581b6d..e3c7f4fc3 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -34,6 +34,9 @@ Arguments agree_car {_} _.
 Arguments agree_not_nil {_} _.
 Local Coercion agree_car : agree >-> list.
 
+Definition to_agree {A} (a : A) : agree A :=
+  {| agree_car := [a]; agree_not_nil := eq_refl |}.
+
 Lemma elem_of_agree {A} (x : agree A) : ∃ a, a ∈ agree_car x.
 Proof. destruct x as [[|a ?] ?]; set_solver+. Qed.
 Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y → x = y.
@@ -156,9 +159,6 @@ Proof.
     apply discrete_iff_0; auto.
 Qed.
 
-Program Definition to_agree (a : A) : agree A :=
-  {| agree_car := [a]; agree_not_nil := eq_refl |}.
-
 Global Instance to_agree_ne : NonExpansive to_agree.
 Proof.
   intros n a1 a2 Hx; split=> b /=;
-- 
GitLab