diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 889d1057c2bbfbcec7d689d03b13418745c24275..2410b2f6e84a8c03e06e8c258511402dc19ca2ed 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 *)