diff --git a/theories/tactics.v b/theories/tactics.v
index 3b9f8a182427db46eef823006b2af68310c27b00..ff8306f34dabda515ff46ce4d1dff42345ac5805 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -76,7 +76,7 @@ Ltac done_if b :=
   | false => idtac
   end.
 
-(** Aliases for trans and etrans that are easier to type *)
+(** Aliases for transitivity and etransitivity that are easier to type *)
 Tactic Notation "trans" constr(A) := transitivity A.
 Tactic Notation "etrans" := etransitivity.