From 14f857ba53874210ae277788d3b6c57a1ca40ad1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 14 Dec 2016 08:52:22 +0100
Subject: [PATCH] add comment on dec_agree in evmap

---
 theories/evmap.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/evmap.v b/theories/evmap.v
index 48a65f1..22e6677 100644
--- a/theories/evmap.v
+++ b/theories/evmap.v
@@ -6,6 +6,11 @@ From iris.algebra Require deprecated.
 From iris.proofmode Require Import tactics.
 
 Export deprecated.dec_agree.
+(* Porting this to algebra.agree does not really work well because the
+   map from K to (Q * agree A) is part of the interface of this file.
+   This file should either be ditched or raised to a higher level
+   of abstraction, i.e., work on a map from K to A and use fmap
+   for the thing that's owned. *)
 
 Section evmap.
   Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}.
-- 
GitLab