From 7b0417adf5bdcc84543d436c3244aba9ea65befb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 13:58:34 +0100
Subject: [PATCH] ...

---
 algebra/agree.v     | 2 +-
 algebra/dec_agree.v | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/algebra/agree.v b/algebra/agree.v
index 7b8641655..a71d7a4d2 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -61,7 +61,7 @@ Instance agree_unit : Unit (agree A) := id.
 Instance agree_minus : Minus (agree A) := λ x y, x.
 Instance: Comm (≡) (@op (agree A) _).
 Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
-Definition agree_idemp (x : agree A) : x ⋅ x ≡ x.
+Lemma agree_idemp (x : agree A) : x ⋅ x ≡ x.
 Proof. split; naive_solver. Qed.
 Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
 Proof.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 9683f606f..3adbb7eef 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -47,3 +47,5 @@ Proof.
 Qed.
 
 Canonical Structure dec_agreeRA : cmraT := discreteRA dec_agree_ra.
+
+End dec_agree.
\ No newline at end of file
-- 
GitLab