Add reference to discussions

Discussions at https://github.com/mit-plv/fiat-crypto/issues/164 and https://github.com/mit-plv/fiat-crypto/pull/163

1 files changed, 6 insertions, 0 deletions

diff --git a/src/Util/ForLoop.v b/src/Util/ForLoop.v
index 9ec6f5ba4..db12608e2 100644
--- a/src/Util/ForLoop.v
+++ b/src/Util/ForLoop.v
@@ -1,6 +1,12 @@
 (** * Definition and Notations for [for (int i = i₀; i < i∞; i += Δi)] *)
 Require Import Coq.ZArith.BinInt.
 Require Import Crypto.Util.Notations.
+(** Note: These definitions are fairly tricky.  See
+    https://github.com/mit-plv/fiat-crypto/issues/164 and
+    https://github.com/mit-plv/fiat-crypto/pull/163 for more
+    discussion.
+
+    TODO: Fix the definitions to make them more obviously right. *)
 
 Section with_body.
   Context {stateT : Type}