diff --git a/theories/tactics.v b/theories/tactics.v
index de800da122dde4d9cb8c54cf957a70316d799e77..78dbd9788085203f1174404ee0883e7442e05bdb 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -239,7 +239,7 @@ Ltac mk_evar T :=
   e'.
 
 (** The tactic [get_head t] returns the head function [f] when [t] is of the
-shape [f a1 ... aN]. *)
+shape [f a1 ... aN]. This is purely syntactic, no unification is performed. *)
 Ltac get_head e :=
   lazymatch e with
   | ?h _ => get_head h