Robbert Krebbers
--- a/theories/base.v
+++ b/theories/base.v
 Existing Instance TCElemOf_further.
 Hint Mode TCElemOf ! ! ! : typeclass_instances.

-(** Similarly to [TCForall2], we declare the modes of [TCEq x y] in both
-directions, i.e., either [x] input and [y] output, or [y] input and [x]
-output. *)
+(** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
+[TCEq] can also be used to unify evars. This is harmless: since the only
+instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See
+https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *)