From c5f3fc77c7851d6f40ffb4f56f21da716fab7d1b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Feb 2016 16:05:18 +0100
Subject: [PATCH] Correct implicit arguments dec_agree.

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

diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 89c76616e..753bc8073 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -52,5 +52,6 @@ Proof. destruct x; by repeat (simplify_eq/= || case_match). Qed.
 
 Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 ≡ x2.
 Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
-
 End dec_agree.
+
+Arguments dec_agreeRA _ {_}.
-- 
GitLab