adapt to coq#19611

math-comp · Oct 30, 2024 · 1b3de38 · 1b3de38
1 parent 1753715
commit 1b3de38
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/classical/functions.v b/classical/functions.v
@@ -1253,7 +1253,7 @@ Lemma odflt_unbind : odflt x = unbind (fun=> x) idfun. Proof. by []. Qed.
 HB.instance Definition _ := Inv.Build _ _ (odflt x) some.
 
 HB.instance Definition _ := SplitBij.copy (odflt x)
-  [the {bij some @` A >-> A} of unbind (fun=> x) idfun].
+  [the {splitbij some @` A >-> A} of @unbind (option T) T (fun=> x) idfun].
 
 End Odflt.
 

diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -40,7 +40,7 @@ Lemma ler_sqrt {R : rcfType} (a b : R) :
   (0 <= b -> (Num.sqrt a <= Num.sqrt b) = (a <= b))%R.
 Proof.
 have [b_gt0 _|//|<- _] := ltgtP; last first.
-  by rewrite sqrtr0 -sqrtr_eq0 le_eqVlt ltNge sqrtr_ge0 orbF.
+  by rewrite sqrtr0 -[RHS]sqrtr_eq0 le_eqVlt ltNge sqrtr_ge0 orbF.
 have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt// ?qualifE/= ?ltW.
 by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0) ?ltW.
 Qed.

diff --git a/theories/exp.v b/theories/exp.v
@@ -974,7 +974,7 @@ have ap0 : (0 < a `^ p)%R by rewrite powR_gt0.
 have bq0 : (0 < b `^ q)%R by rewrite powR_gt0.
 have := @concave_ln _ (@Itv.mk _ `[0, 1] _ q01)%R _ _ ap0 bq0.
 have pq' : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK.
-rewrite !convRE/= /onem -pq' -ler_expR expRD (mulrC p^-1).
+rewrite !convRE/= /onem -pq' -[_ <= ln _]ler_expR expRD (mulrC p^-1).
 rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF// (mulrC q^-1).
 rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF//.
 rewrite lnK ?posrE// lnK ?posrE// => /le_trans; apply.