diff options
| -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 0382d30666..5def8d84a1 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. |