From 65b9ce9f73eb1c4069baf4dfd779d1c307d36070 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Jan 2017 17:33:59 +0100
Subject: [PATCH] Document list_remove and list_remove_list.

---
 theories/prelude/list.v | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/theories/prelude/list.v b/theories/prelude/list.v
index 8ef98f665..7228aa6f1 100644
--- a/theories/prelude/list.v
+++ b/theories/prelude/list.v
@@ -285,18 +285,20 @@ Inductive contains {A} : relation (list A) :=
 Infix "`contains`" := contains (at level 70) : C_scope.
 Hint Extern 0 (_ `contains` _) => reflexivity.
 
-Section contains_dec_help.
-  Context `{EqDecision A}.
-  Fixpoint list_remove (x : A) (l : list A) : option (list A) :=
-    match l with
-    | [] => None
-    | y :: l => if decide (x = y) then Some l else (y ::) <$> list_remove x l
-    end.
-  Fixpoint list_remove_list (k : list A) (l : list A) : option (list A) :=
-    match k with
-    | [] => Some l | x :: k => list_remove x l ≫= list_remove_list k
-    end.
-End contains_dec_help.
+(** Removes [x] from the list [l]. The function returns a [Some] when the
++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
+  | y :: l => if decide (x = y) then Some l else (y ::) <$> list_remove x l
+  end.
+
+(** Removes all elements in the list [k] from the list [l]. The function returns
+a [Some] when the removal succeeds and [None] some element of [k] is not in [l]. *)
+Fixpoint list_remove_list `{EqDecision A} (k : list A) (l : list A) : option (list A) :=
+  match k with
+  | [] => Some l | x :: k => list_remove x l ≫= list_remove_list k
+  end.
 
 Inductive Forall3 {A B C} (P : A → B → C → Prop) :
      list A → list B → list C → Prop :=
-- 
GitLab