diff --git a/theories/list.v b/theories/list.v
index b78ba495a5ac39dcd8daa24743185c7de4e1a556..0d55033590d6c582b4cdf36493bec13a86528d3f 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -327,7 +327,7 @@ Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
 Global Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
 
 (** Removes [x] from the list [l]. The function returns a [Some] when the
-+removal succeeds and [None] when [x] is not in [l]. *)
+removal succeeds and [None] when [x] is not in [l]. *)
 Fixpoint list_remove `{EqDecision A} (x : A) (l : list A) : option (list A) :=
   match l with
   | [] => None