list_eq_dec now transparent (wish #2786)

 The proof is also replaced by a mere "decide equality".
 Patch by Robbert Krebbers.

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

1 files changed, 2 insertions, 13 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 69375f4a8d..7296d07ec3 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -827,22 +827,11 @@ Section ListOps.
 
   Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}.
 
-  Lemma list_eq_dec :
-    forall l l':list A, {l = l'} + {l <> l'}.
-  Proof.
-    induction l as [| x l IHl]; destruct l' as [| y l'].
-    left; trivial.
-    right; apply nil_cons.
-    right; unfold not; intro HF; apply (nil_cons (sym_eq HF)).
-    destruct (eq_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql'];
-      try (right; unfold not; intro HF; injection HF; intros; contradiction).
-    rewrite xeqy; rewrite leql'; left; trivial.
-  Qed.
-
+  Lemma list_eq_dec : forall l l':list A, {l = l'} + {l <> l'}.
+  Proof. decide equality. Defined.
 
 End ListOps.
 
-
 (***************************************************)
 (** * Applying functions to the elements of a list *)
 (***************************************************)