From 0721fd0d12784af9d4b8e94e89fe0fa12e180fae Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2022 18:15:01 +0100
Subject: [PATCH] Document FIXME.

---
 iris/program_logic/adequacy.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 59c8e430d..72f78ee78 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -231,6 +231,8 @@ Proof.
   iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
   rewrite -plus_n_O.
   iApply ("Hφ" with "[//] [%] [ ] Hσ Hes'");
+    (* FIXME: Different implicit types for [length] are inferred, so [lia] and
+    [congruence] do not work due to https://github.com/coq/coq/issues/16634 *)
     [by rewrite Hlen1 Hlen3| |]; last first.
   { by rewrite big_sepL2_replicate_r // big_sepL_omap. }
   (* we run the adequacy proof again to get this assumption *)
-- 
GitLab