From 88c02e02a7b6067c78608e9ea526f81fd122edab Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Tue, 14 Mar 2017 16:22:48 +0100
Subject: Fix 3 unused-intro-pattern warnings in stdlib.

---
 theories/Lists/List.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Lists')

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 30f1dec22..1aece3f60 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -419,7 +419,7 @@ Section Elts.
   Proof.
     unfold lt; induction n as [| n hn]; simpl.
     - destruct l; simpl; [ inversion 2 | auto ].
-    - destruct l as [| a l hl]; simpl.
+    - destruct l; simpl.
       * inversion 2.
       * intros d ie; right; apply hn; auto with arith.
   Qed.
@@ -1280,7 +1280,7 @@ End Fold_Right_Recursor.
     partition l = ([], []) <-> l = [].
   Proof.
     split.
-    - destruct l as [|a l' _].
+    - destruct l as [|a l'].
       * intuition.
       * simpl. destruct (f a), (partition l'); now intros [= -> ->].
     - now intros ->.
-- 
cgit v1.2.3