From 531d88c116c76dbfdfb87830ce2f21ebbc0c8a98 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 2 Feb 2016 13:57:17 +0100
Subject: [PATCH] give the fold_left version of fill

---
 barrier/heap_lang.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 889d1057c..2410b2f6e 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -136,7 +136,9 @@ Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
   end.
 
 Fixpoint fill K e :=
-  (* FIXME RJ: This really is fold_left, but if I use that all automation breaks. *)
+  (* FIXME RJ: This really is fold_left, but if I use that all automation breaks:
+       fold_left (fun e Ki => ectx_item_fill Ki e).
+     Or maybe we even have a combinator somewhere to swap the arguments? *)
   match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end.
 
 (** The stepping relation *)
-- 
GitLab