Ajout de fonctions sur les listes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8632 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 0 deletions

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 9d3581a5c..f43aeeddd 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -229,6 +229,18 @@ Proof.
  destruct l2; auto.
 Qed.
 
+Section Remove.
+
+Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
+
+Fixpoint removeA : (x : A) (l : list A){struct l} : list A :=
+  match l with
+    | nil => nil
+    | y::tl => if (eqA_dec x y) then removeA tl else y::(removeA tl)
+  end.
+
+End Remove.
+
 End Type_with_equality.
 
 Hint Constructors InA.