From 43524c6689f372b32770c20d19866f2f4edb4cc6 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 14 Mar 2017 16:22:24 +0100
Subject: Show unused-intro-pattern warning.

This warning was shown in CoqIDE but not by coqc.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9d64e7c599..f186f6e0ec 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3010,7 +3010,7 @@ let warn_unused_intro_pattern =
 	 (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
 
 let check_unused_names names =
-  if not (List.is_empty names) && Flags.is_verbose () then
+  if not (List.is_empty names) then
     warn_unused_intro_pattern names
 
 let intropattern_of_name gl avoid = function
-- 
cgit v1.2.3


From 88c02e02a7b6067c78608e9ea526f81fd122edab Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 14 Mar 2017 16:22:48 +0100
Subject: Fix 3 unused-intro-pattern warnings in stdlib.

---
 theories/Lists/List.v    | 4 ++--
 theories/QArith/Qround.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 30f1dec22c..1aece3f60b 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 ->.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 0ed6d557c0..e94ef408db 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -141,7 +141,7 @@ Qed.
 Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m).
 Proof.
  unfold Qfloor. intros. simpl.
- destruct m as [?|?|p]; simpl.
+ destruct m as [ | | p]; simpl.
   now rewrite Zdiv_0_r, Z.mul_0_r.
   now rewrite Z.mul_1_r.
  rewrite <- Z.opp_eq_mul_m1.
-- 
cgit v1.2.3