From d84c26fa2eeeeb0029a56bac37bf1bae9f10882a Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Mon, 9 Nov 2020 13:01:18 +0100
Subject: Intro pattern extensions for dup, swap and apply

---
 mathcomp/algebra/ssrnum.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index a2a2395..fc24a4b 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1678,7 +1678,7 @@ Hint Resolve real1 : core.
 Lemma realn n : n%:R \is @real R. Proof. by rewrite ger0_real. Qed.
 
 Lemma ler_leVge x y : x <= 0 -> y <= 0 -> (x <= y) || (y <= x).
-Proof. by rewrite -!oppr_ge0 => /(ger_leVge _) h /h; rewrite !ler_opp2. Qed.
+Proof. by rewrite -!oppr_ge0 => /(ger_leVge _) /[apply]; rewrite !ler_opp2. Qed.
 
 Lemma real_leVge x y : x \is real -> y \is real -> (x <= y) || (y <= x).
 Proof. by rewrite -comparabler0 -comparable0r => /comparabler_trans P/P. Qed.
-- 
cgit v1.2.3