diff --git a/tests/telescopes.v b/tests/telescopes.v
index e1836724996f8280a47053aac2934fce5907b9cc..d231e29188b5ea3d5da6f0ca130643a23559640e 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -56,6 +56,9 @@ Proof. by rewrite texist_exist. Qed.
 (** [tele_arg ..] notation tests.
     These tests mainly test type annotations and casts in the [tele_arg]
     notations.
+    We test that Coq can typecheck literal telescope arguments in two ways:
+    - tactic unification/old unification using [exact]
+    - evarconv/new unification using [refine]
  *)
 Example tele_arg_notation_0 : [tele].
 assert_succeeds exact [tele_arg].