From 68f6f9cf169bee5d2fbc3a70556e7e4514f754ce Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 18 Jul 2022 14:23:22 +0200 Subject: [PATCH] Fix broken comment. --- theories/list.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/list.v b/theories/list.v index b78ba495..0d550335 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 -- GitLab