From afc4f47d56af7d5407acbfd3833527c34eb6e894 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 10 Apr 2010 16:30:44 +0000
Subject: Granting wish #2229 (InA_dec transparent) and Michael Day's coq-club
 8 April 2010 wish (addition of map_eq_nil).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12919 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/List.v       | 5 +++++
 theories/Lists/SetoidList.v | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index b3e37685bb..766456fff7 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -825,6 +825,11 @@ Section Map.
     rewrite IHl; auto.
   Qed.
 
+  Lemma map_eq_nil : forall l, map l = [] -> l = [].
+  Proof.
+    destruct l; simpl; reflexivity || discriminate.
+  Qed.
+
   (** [flat_map] *)
 
   Definition flat_map (f:A -> list B) :=
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 2aecb3fdbf..d42e71e556 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -489,7 +489,7 @@ left; auto.
 destruct IHl.
 left; auto.
 right; intro; inv; contradiction.
-Qed.
+Defined.
 
 Fixpoint removeA (x : A) (l : list A) : list A :=
   match l with
-- 
cgit v1.2.3