diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-15 22:29:26 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-15 22:29:26 +0000 |
commit | 15a7e0b3e4af14dc965f48b39436b42f3620988d (patch) | |
tree | 2443cbcc17ebbdfb1b93b5e3673c26d1f164eb53 /theories/Lists/SetoidList.v | |
parent | 07afe4dec5b099f3277c6818e464885f7211db06 (diff) |
Typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/SetoidList.v')
-rw-r--r-- | theories/Lists/SetoidList.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index f43aeeddd..c65ea3562 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -233,10 +233,10 @@ 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 := +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) + | y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl) end. End Remove. |