Fix flat_map definition so that it plays nicely with fix

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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 228661ec6..37802d4bc 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1102,11 +1102,11 @@ Section Map.
 
   (** [flat_map] *)
 
-  Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} :
-    list B :=
+  Definition flat_map (f:A -> list B) :=
+    fix flat_map (l:list A) {struct l} : list B :=
     match l with
       | nil => nil
-      | cons x t => (f x)++(flat_map f t)
+      | cons x t => (f x)++(flat_map t)
     end.
 
   Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),