diff --git a/theories/list.v b/theories/list.v
index c6e0aeb46f6a221536ac07d3a6ea4ad44218c551..05465e2b0b07cdf0c590869620efe1b4e3cf5dcc 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2713,7 +2713,7 @@ Proof.
 Defined.
 
 (** Export the Coq stdlib constructors under different names,
-because we use Forall_nil and Forall_cons for a version with a biimplication. *)
+because we use [Forall_nil] and [Forall_cons] for a version with a biimplication. *)
 Definition Forall_nil_2 := @Forall_nil A.
 Definition Forall_cons_2 := @Forall_cons A.
 Global Instance Forall_proper:
@@ -2986,7 +2986,7 @@ Lemma Forall2_Forall {A} P (l1 l2 : list A) :
 Proof. induction 1; constructor; auto. Qed.
 
 (** Export the Coq stdlib constructors under a different name,
-because we use Forall_nil and Forall_cons for a version with a biimplication. *)
+because we use [Forall2_nil] and [Forall2_cons] for a version with a biimplication. *)
 Definition Forall2_nil_2 := @Forall2_nil.
 Definition Forall2_cons_2 := @Forall2_cons.
 Section Forall2.