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/QArith/Qround.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/QArith') diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 0ed6d557c..e94ef408d 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