diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-15 22:23:31 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-15 22:23:31 +0000 |
commit | 07afe4dec5b099f3277c6818e464885f7211db06 (patch) | |
tree | f4a1d4a420d95e3647c1b003b1f0488e136903ba | |
parent | 84592f2d128fcb322a59b40bb4ce6dc6e388943f (diff) |
Typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8633 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/Lists/MoreList.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Lists/MoreList.v b/theories/Lists/MoreList.v index 0382d3066..5def8d84a 100644 --- a/theories/Lists/MoreList.v +++ b/theories/Lists/MoreList.v @@ -469,10 +469,10 @@ Section Remove. Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. -Fixpoint remove : (x : A) (l : list A){struct l} : list A := +Fixpoint remove (x : A) (l : list A){struct l} : list A := match l with | nil => nil - | y::tl => if (eq_dec x y) then remove tl else y::(remove tl) + | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) end. End Remove. |