From ac6f5d18ce47df8cb8bd4b7e720f0b616b5b5e2c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 27 Nov 2017 13:18:36 +0100
Subject: [PATCH] Do not name constructor of `agree`; it should never be used.

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

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 2a6b94f84..78c581b6d 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -26,11 +26,10 @@ Proof.
   Thus Ag(T) is not necessarily complete.
 *)
 
-Record agree (A : Type) : Type := Agree {
+Record agree (A : Type) : Type := {
   agree_car : list A;
   agree_not_nil : bool_decide (agree_car = []) = false
 }.
-Arguments Agree {_} _ _.
 Arguments agree_car {_} _.
 Arguments agree_not_nil {_} _.
 Local Coercion agree_car : agree >-> list.
@@ -82,7 +81,7 @@ Instance agree_validN : ValidN (agree A) := λ n x,
 Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
 
 Program Instance agree_op : Op (agree A) := λ x y,
-  Agree (agree_car x ++ agree_car y) _.
+  {| agree_car := agree_car x ++ agree_car y |}.
 Next Obligation. by intros [[|??]] y. Qed.
 Instance agree_pcore : PCore (agree A) := Some.
 
-- 
GitLab