Merge pull request #32 from math-comp/prepare_release_1.1.2

update scripts to mathcomp 1.11 + fix namespace

_CoqProject

@@ -10,3 +10,11 @@ theories/realalg.v
 theories/mxtens.v
 
 -R theories mathcomp.real_closed
+-arg -w -arg -projection-no-head-constant
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -notation-overridden
+-arg -w -arg +duplicate-clear
+-arg -w -arg +non-primitive-record
+-arg -w -arg +undeclared-scope
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -uniform-inheritance

meta.yml

@@ -80,7 +80,7 @@ dependencies:
   description: |-
     [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
 
-namespace: mathcomp
+namespace: mathcomp.real_closed
 
 keywords:
 - name: real closed field

theories/cauchyreals.v

@@ -21,6 +21,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope creal_scope.
 Delimit Scope creal_scope with CR.
 
 Section poly_extra.
@@ -43,7 +44,7 @@ Lemma size_nderivn (R : realDomainType) (p : {poly R}) n :
   size p^`N(n) = (size p - n)%N.
 Proof.
 rewrite -size_derivn nderivn_def -mulr_natl.
-by rewrite -polyC1 -!polyC_muln size_Cmul // pnatr_eq0 -lt0n fact_gt0.
+by rewrite -polyC1 -!polyCMn size_Cmul // pnatr_eq0 -lt0n fact_gt0.
 Qed.
 
 End poly_extra.
@@ -531,7 +532,7 @@ Lemma splitf (n : nat) (e : F) : e = iterop n +%R (e / n%:R) e.
 Proof.
 case: n=> // n; set e' := (e / _).
 have -> : e = e' * n.+1%:R by rewrite mulfVK ?pnatr_eq0.
-move: e'=> {e} e; rewrite iteropS.
+move: e'=> {}e; rewrite iteropS.
 by elim: n=> /= [|n <-]; rewrite !mulr_natr ?mulr1n.
 Qed.
 
@@ -694,7 +695,7 @@ Proof.
 apply: eq_crealP; exists (fun _ => 0%N).
 by move=> e i e_gt0 _; rewrite subrr normr0.
 Qed.
-Hint Resolve eq_creal_refl.
+Hint Resolve eq_creal_refl : core.
 
 Lemma neq_creal_sym x y : x != y -> y != x.
 Proof.
@@ -802,7 +803,7 @@ Qed.
 
 Lemma le_creal_refl (x : creal) : (x <= x)%CR.
 Proof. by apply: (@le_crealP 0%N). Qed.
-Hint Resolve le_creal_refl.
+Hint Resolve le_creal_refl : core.
 
 Lemma lt_neq_creal (x y : creal) : (x < y)%CR -> x != y.
 Proof.
@@ -1300,7 +1301,7 @@ have cop_q'_d': coprimep p' q'.
   by rewrite (dvdp_trans (dvdp_gcdr _ _)) ?dvdp_gdco.
 suff : (p' * q').[x]  * (d ^+ (size p + size q)).[x] == 0.
   case/poly_mul_creal_eq0_coprime.
-  + by rewrite coprimep_expr // coprimep_mull ?coprimep_gdco.
+  + by rewrite coprimep_expr // coprimepMl ?coprimep_gdco.
   + move=> p'q'x_eq0.
     have : p'.[x] * q'.[x] == 0 by rewrite -horner_crealM.
     case/poly_mul_creal_eq0_coprime=> // /dvdp_creal_eq0 hp'q'.
@@ -1493,7 +1494,7 @@ rewrite ger0_norm; last first.
 rewrite size_norm_poly2 ler_sum //= => l _.
 rewrite !{1}coef_nderivn normrMn ler_pmuln2r ?bin_gt0 ?leq_addr //.
 rewrite -!polyC_exp !coefMC coef_norm_poly2 normrM ler_wpmul2l ?normr_ge0 //.
-rewrite normrX; case: (val l)=> // {l} l.
+rewrite normrX; case: (val l)=> // {}l.
 by rewrite ler_pexpn2r -?topredE //= ?uboundP ?ltW ?ubound_gt0.
 Qed.
 
@@ -1670,8 +1671,7 @@ Notation "x ^+ n" := (exp_creal x n) : creal_scope.
 
 Notation "`| x |" := (norm_creal x) : creal_scope.
 
-Hint Resolve eq_creal_refl.
-Hint Resolve le_creal_refl.
+#[global] Hint Resolve eq_creal_refl le_creal_refl : core.
 
 Notation lbound_of p := (@lboundP _ _ _ p _ _ _).
 Notation lbound0_of p := (@lbound0P _ _ p _ _ _).

theories/complex.v

@@ -7,6 +7,7 @@ From mathcomp
 Require Import bigop order ssralg ssrint div ssrnum rat poly closed_field.
 From mathcomp
 Require Import polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg.
+From mathcomp Require Import mxpoly.
 
 (**********************************************************************)
 (*   This files defines the extension R[i] of a real field R,         *)
@@ -37,6 +38,7 @@ Local Notation sqrtr := Num.sqrt.
 
 Record complex (R : Type) : Type := Complex { Re : R; Im : R }.
 
+Declare Scope complex_scope.
 Delimit Scope complex_scope with C.
 Local Open Scope complex_scope.
 
@@ -797,7 +799,7 @@ rewrite !xpair_eqE /= [_ == i']eq_sym [_ == j']eq_sym (negPf neq'_ij) /=.
 set z := (_ && _); suff /negPf -> : ~~ z by rewrite subrr mulr0.
 by apply: contraL lt_j'i' => /andP [/eqP <- /eqP <-]; rewrite ltnNge ltnW.
 Qed.
-Hint Resolve skew_direct_sum.
+Hint Resolve skew_direct_sum : core.
 
 Lemma rank_skew : \rank skew = (n * n.-1)./2.
 Proof.
@@ -1054,7 +1056,7 @@ pose L2fun : 'M[R]_n -> _ :=
            \+ ((mulmx (u^T) \o trmx)               \+ (mulmx (v^T)))).
 pose L2 := lin_mx [linear of L2fun].
 have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _).
-+ by move: HrV; rewrite mxrank1 !dvdn2 ?negbK odd_mul andbb.
++ by move: HrV; rewrite mxrank1 !dvdn2 ?negbK oddM andbb.
 + by move=> ? _ /=; rewrite submx1.
 + suff {f fE}: L1 *m L2 = L2 *m L1.
     move: L1 L2 => L1 L2 commL1L2 La Lb.
@@ -1131,7 +1133,7 @@ have [] /= := IHk _ (leqnn _) _  _ (skew R[i] n.+1) _ [::L1; L2] (erefl _).
 + rewrite rank_skew; apply: contra Hn.
   rewrite -(@dvdn_pmul2r 2) //= -expnSr muln2 -[_.*2]add0n.
   have n_odd : odd n by rewrite dvdn2 /= ?negbK in dvd2n *.
-  have {2}<- : odd (n.+1 * n) = 0%N :> nat by rewrite odd_mul /= andNb.
+  have {2}<- : odd (n.+1 * n) = 0%N :> nat by rewrite oddM /= andNb.
   by rewrite odd_double_half Gauss_dvdl // coprime_pexpl // coprime2n.
 + move=> L; rewrite 2!in_cons in_nil orbF => /orP [] /eqP ->;
   apply/rV_subP => v /submxP [s -> {v}]; rewrite mulmxA; apply/skewP;

theories/ordered_qelim.v

@@ -79,7 +79,7 @@ Canonical term_eqType (T : eqType) :=
 Arguments term_eqP T {x y}.
 Prenex Implicits term_eq.
 
-
+Declare Scope oterm_scope.
 Bind Scope oterm_scope with term.
 Bind Scope oterm_scope with formula.
 Delimit Scope oterm_scope with oT.
@@ -169,6 +169,7 @@ Definition le_of_oclause (R : Type) (x : oclause R) :=
 
 End OrderedClause.
 
+Declare Scope oclause_scope.
 Delimit Scope oclause_scope with OCLAUSE.
 Open Scope oclause_scope.
 
@@ -364,60 +365,60 @@ split=> t1.
 - rewrite /eq0_rform; move: (ub_var t1) => m.
   set tr := _ m.
   suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR.
-    case: tr => {t1} t1 r /= /andP[t1_r].
+    case: tr => {}t1 r /= /andP[t1_r].
     by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr.
   have: all (@rterm R) [::] by [].
   rewrite {}/tr; elim: t1 [::] => //=.
   + move=> t1 IHt1 t2 IHt2 r.
-  move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r].
-  move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r].
+  move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r].
+  move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r].
   by rewrite t1_r t2_r.
   + by move=> t1 IHt1 r /IHt1; case: to_rterm.
   + by move=> t1 IHt1 n r /IHt1; case: to_rterm.
   + move=> t1 IHt1 t2 IHt2 r.
-  move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r].
-  move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r].
+  move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r].
+  move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r].
   by rewrite t1_r t2_r.
   + move=> t1 IHt1 r.
-  by move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /=; rewrite all_rcons.
+  by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons.
   + by move=> t1 IHt1 n r /IHt1; case: to_rterm.
 - rewrite /lt0_rform; move: (ub_var t1) => m; set tr := _ m.
   suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR.
-    case: tr => {t1} t1 r /= /andP[t1_r].
+    case: tr => {}t1 r /= /andP[t1_r].
     by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr.
   have: all (@rterm R) [::] by [].
   rewrite {}/tr; elim: t1 [::] => //=.
   + move=> t1 IHt1 t2 IHt2 r.
-  move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r].
-  move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r].
+  move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r].
+  move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r].
   by rewrite t1_r t2_r.
   + by move=> t1 IHt1 r /IHt1; case: to_rterm.
   + by move=> t1 IHt1 n r /IHt1; case: to_rterm.
   + move=> t1 IHt1 t2 IHt2 r.
-  move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r].
-  move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r].
+  move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r].
+  move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r].
   by rewrite t1_r t2_r.
   + move=> t1 IHt1 r.
-  by move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /=; rewrite all_rcons.
+  by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons.
   + by move=> t1 IHt1 n r /IHt1; case: to_rterm.
 - rewrite /leq0_rform; move: (ub_var t1) => m; set tr := _ m.
   suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR.
-    case: tr => {t1} t1 r /= /andP[t1_r].
+    case: tr => {}t1 r /= /andP[t1_r].
     by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr.
   have: all (@rterm R) [::] by [].
   rewrite {}/tr; elim: t1 [::] => //=.
   + move=> t1 IHt1 t2 IHt2 r.
-  move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r].
-  move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r].
+  move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r].
+  move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r].
   by rewrite t1_r t2_r.
   + by move=> t1 IHt1 r /IHt1; case: to_rterm.
   + by move=> t1 IHt1 n r /IHt1; case: to_rterm.
   + move=> t1 IHt1 t2 IHt2 r.
-  move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r].
-  move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r].
+  move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r].
+  move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r].
   by rewrite t1_r t2_r.
   + move=> t1 IHt1 r.
-  by move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /=; rewrite all_rcons.
+  by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons.
   + by move=> t1 IHt1 n r /IHt1; case: to_rterm.
 Qed.
 
@@ -546,8 +547,8 @@ elim: t r0 m => /=; try do [
    first by [rewrite takel_cat // -htake1 size_take geq_minr];
   rewrite -(rsub_acc r1 r3 t1') {hub1'}// -{htake1}htake2 {r3}cat_take_drop;
   by elim: r2 m => //= u r2 IHr2 m; rewrite IHr2
-| do [ move=> t1 IHt1 r m; do 2!move/IHt1=> {IHt1}IHt1
-     | move=> t1 IHt1 n r m; do 2!move/IHt1=> {IHt1}IHt1];
+| do [ move=> t1 IHt1 r m; do 2!move/IHt1=> {}IHt1
+     | move=> t1 IHt1 n r m; do 2!move/IHt1=> {}IHt1];
   case: to_rterm IHt1 => t1' r1 [-> -> hsub1 <-]; split=> {hsub1}//;
   by elim: r1 m => //= u r1 IHr1 m; rewrite IHr1].
 move=> t1 IH r m letm /IH {IH} /(_ letm) {letm}.
@@ -715,7 +716,7 @@ have and_ok bcs1 bcs2: ok bcs1 -> ok bcs2 -> ok (and_odnf bcs1 bcs2).
   case/and3P=> ok11 ok12 ok1 ok2; rewrite cat_ok ?{}IH1 {bcs1 ok1}//.
   elim: bcs2 ok2 => //= cl2 bcs2 IH2 /andP[ok2 /IH2->].
   by rewrite /dnf_rterm /= !all_cat andbT ok11; case/and3P: ok12=> -> -> ->.
-elim: f b => //=; try by [move=> _ ? ? [] | move=> ? ? ? ? [] /= /andP[]; auto].
+elim: f b => //=; do ?by [move=> ? ? ? [] | move=> ? ? ? ? [] /= /andP[]; auto].
 - by do 2!case.
 - by rewrite /dnf_rterm => ? ? [] /= ->.
 - by rewrite /dnf_rterm => ? ? [] /=; rewrite andbC !andbT.
@@ -1034,7 +1035,7 @@ rewrite /oclause_to_w /= !all_map.
 apply/allP => [] [oc_eq oc_neq oc_le oc_lt] hoc; rewrite /dnf_rterm /= andbT.
 rewrite -all_cat; apply/allP=> u hu; move/terms_of_neq_leq_elim: hoc => /=.
 move/(_ u); rewrite !mem_cat.
-have {hu} hu : [|| u \in oc_eq, u \in oc_neq, u \in oc_le | u \in oc_lt].
+have {}hu : [|| u \in oc_eq, u \in oc_neq, u \in oc_le | u \in oc_lt].
   by move: hu; rewrite mem_cat; case/orP=> ->; rewrite ?orbT.
 move/(_ hu); case/orP; last first.
   move: rneq.
@@ -1083,7 +1084,7 @@ have -> :
 move: (dnf_rterm_subproof hdnf).
 rewrite /oclause_to_w; elim: (oclause_neq_leq_elim bc) => /= [|a l ih].
   by split=> //; case.
-case/andP=> h1 h2; have {ih h2} ih := (ih h2); split.
+case/andP=> h1 h2; have {h2} ih := (ih h2); split.
 - case/orP.
     move/(valid_QE_wproj i e h1)=> /= [x /=] [] // [] h2 [] _ [] h3 _; exists x.
     by left.

theories/polyorder.v

@@ -164,7 +164,7 @@ Qed.
 
 Lemma mu_opp p x : \mu_x (-p) = \mu_x p.
 Proof.
-rewrite -mulN1r -polyC1 -polyC_opp mul_polyC mu_mulC //.
+rewrite -mulN1r -polyC1 -polyCN mul_polyC mu_mulC //.
 by rewrite -oppr0 (inj_eq (inv_inj (@opprK _))) oner_eq0.
 Qed.
 

theories/polyrcf.v

@@ -115,7 +115,7 @@ Section SgpInfty.
 Lemma sgp_pinfty_sym p : sgp_pinfty (p \Po -'X) = sgp_minfty p.
 Proof.
 rewrite /sgp_pinfty /sgp_minfty lead_coef_comp ?size_opp ?size_polyX //.
-by rewrite lead_coef_opp lead_coefX mulrC.
+by rewrite lead_coefN lead_coefX mulrC.
 Qed.
 
 Lemma poly_pinfty_gt_lc p :
@@ -197,22 +197,22 @@ Proof.
 move=> p_neq0 x; rewrite in_itv /=; apply/contra_leN.
 by case/rootP/(cauchy_boundP p_neq0)/ltr_normlP; rewrite ltr_oppl.
 Qed.
-Hint Resolve le_cauchy_bound.
+Hint Resolve le_cauchy_bound : core.
 
 Lemma ge_cauchy_bound p : p != 0 -> {in `[cauchy_bound p, +oo[, noroot p}.
 Proof.
 move=> p_neq0 x; rewrite in_itv andbT /=; apply/contra_leN.
 by case/rootP/(cauchy_boundP p_neq0)/ltr_normlP; rewrite ltr_oppl.
 Qed.
-Hint Resolve ge_cauchy_bound.
+Hint Resolve ge_cauchy_bound : core.
 
 Lemma cauchy_bound_gt0 p : cauchy_bound p > 0.
 Proof. by rewrite ltr_spaddl ?ltr01 // mulrC divr_ge0 ?normr_ge0 ?sumr_ge0. Qed.
-Hint Resolve cauchy_bound_gt0.
+Hint Resolve cauchy_bound_gt0 : core.
 
 Lemma cauchy_bound_ge0 p : cauchy_bound p >= 0.
 Proof. by rewrite ltW. Qed.
-Hint Resolve cauchy_bound_ge0.
+Hint Resolve cauchy_bound_ge0 : core.
 
 End CauchyBound.
 
@@ -843,7 +843,7 @@ case: eqVneq => [->|p0]; first by exists [::]; constructor.
 case: (boolP (p^`() == 0)) => [|p'0].
   rewrite -derivn1 -derivn_poly0 => /size1_polyC pC; exists [::].
   by constructor=> // x; rewrite pC rootC -polyC_eq0 -pC (negPf p0) andbF.
-have {ihn} /ihn /(_ a b) [sp'] : (size p^`() <= n)%N.
+have {}/ihn /(_ a b) [sp'] : (size p^`() <= n)%N.
   rewrite -ltnS; apply: leq_trans sp; rewrite size_deriv prednK // lt0n.
   by rewrite size_poly_eq0 p0.
 elim: sp' a => [|r1 sp' hsp'] a hp'.
@@ -896,18 +896,18 @@ Proof. by case: rootsP=> //=; rewrite eqxx. Qed.
 Lemma roots_on_roots : forall p a b, p != 0 ->
   roots_on p `]a, b[ (roots p a b).
 Proof. by move=> a b p; case: rootsP. Qed.
-Hint Resolve roots_on_roots.
+Hint Resolve roots_on_roots : core.
 
 Lemma sorted_roots a b p : sorted <%R (roots p a b).
 Proof. by case: rootsP. Qed.
-Hint Resolve sorted_roots.
+Hint Resolve sorted_roots : core.
 
 Lemma path_roots p a b : path <%R a (roots p a b).
 Proof.
 case: rootsP=> //= p0 hp sp; rewrite path_min_sorted //.
 by apply/allP=> y; rewrite -hp; case/andP => /itvP ->.
 Qed.
-Hint Resolve path_roots.
+Hint Resolve path_roots : core.
 
 Lemma root_is_roots (p : {poly R}) (a b : R) :
    p != 0 -> forall x, x \in `]a, b[ -> root p x = (x \in roots p a b).
@@ -1264,7 +1264,7 @@ have [->|p0] := eqVneq p 0; first by rewrite roots0.
 by apply: (@sorted_uniq _ <%R); [apply: lt_trans | apply: ltxx|].
 Qed.
 
-Hint Resolve uniq_roots.
+Hint Resolve uniq_roots : core.
 
 Lemma in_roots p (a b x : R) :
   (x \in roots p a b) = [&& root p x, x \in `]a, b[ & p != 0].
@@ -1421,7 +1421,7 @@ Proof. by rewrite /sgp_right size_poly0. Qed.
 Lemma sgr_neighpr b p x :
   {in neighpr p x b, forall y, (sgr p.[y] = sgp_right p x)}.
 Proof.
-elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {p} p.
+elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {}p.
   rewrite leqn0 size_poly_eq0 /neighpr; move/eqP=> -> /= y.
   by rewrite next_root0 itv_xx.
 rewrite leq_eqVlt ltnS; case/predU1P => [sp|]; last exact: ihn.
@@ -1461,7 +1461,7 @@ Lemma sgr_neighpl a p x :
     (sgr p.[y] = (-1) ^+ (odd (\mu_x p)) * sgp_right p x)
   }.
 Proof.
-elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {p} p.
+elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {}p.
   rewrite leqn0 size_poly_eq0 /neighpl; move/eqP=> -> /= y.
   by rewrite prev_root0 itv_xx.
 rewrite leq_eqVlt ltnS; case/predU1P => [sp y|]; last exact: ihn.
@@ -1663,7 +1663,7 @@ Lemma rootsRP p a b :
 Proof.
 move=> rpa rpb.
 have [->|p_neq0] := eqVneq p 0; first by rewrite rootsR0 roots0.
-apply: (eq_sorted_irr lt_trans); rewrite ?sorted_roots // => x.
+apply: (irr_sorted_eq lt_trans); rewrite ?sorted_roots // => x.
 rewrite -roots_on_rootsR -?roots_on_roots //=.
 case: (boolP (root _ _)); rewrite ?(andbT, andbF) //.
 apply: contraLR; rewrite in_itv negb_and -!leNgt.
@@ -1677,10 +1677,10 @@ Proof.
 rewrite /sgp_pinfty; wlog lp_gt0 : x p / lead_coef p > 0 => [hwlog|rpx y Hy].
   have [|/(hwlog x p) //|/eqP] := ltrgtP (lead_coef p) 0; last first.
     by rewrite lead_coef_eq0 => /eqP -> ? ? ?; rewrite lead_coef0 horner0.
-  rewrite -[p]opprK lead_coef_opp oppr_cp0 => /(hwlog x _) Hp HNp y Hy.
+  rewrite -[p]opprK lead_coefN oppr_cp0 => /(hwlog x _) Hp HNp y Hy.
   by rewrite hornerN !sgrN Hp => // z /HNp; rewrite rootN.
 have [z Hz] := poly_pinfty_gt_lc lp_gt0.
-have {Hz} Hz u : u \in `[z, +oo[ -> Num.sg p.[u] = 1.
+have {}Hz u : u \in `[z, +oo[ -> Num.sg p.[u] = 1.
   rewrite in_itv andbT => /Hz pu_ge1.
   by rewrite gtr0_sg // (lt_le_trans lp_gt0).
 rewrite (@polyrN0_itv _ _ rpx (maxr y z)) ?in_itv /= ?le_maxr ?(itvP Hy) //.