From 07643798a7651d26f13deb054fb7c83e59613491 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 29 Oct 2009 17:10:06 +0000
Subject: 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
---
 theories/Lists/List.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 228661ec64..37802d4bcf 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),
-- 
cgit v1.2.3