Skip to content

Commit

Permalink
fix for coq.dev
Browse files Browse the repository at this point in the history
  • Loading branch information
@CohenCyril @thery
CohenCyril authored and thery committed Jan 3, 2023
1 parent 1bac34b commit 4bdc918
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 19 deletions.
4 changes: 1 addition & 3 deletions src/freeg.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,8 +75,6 @@ Module FreegDefs.
_ : reduced seq_of_prefreeg
}.

Implicit Arguments mkPrefreeg [].

Local Coercion seq_of_prefreeg : prefreeg >-> seq.

Lemma prefreeg_reduced: forall (D : prefreeg), reduced D.
Expand All @@ -95,7 +93,7 @@ Module FreegDefs.
Canonical prefreeg_choiceType := Eval hnf in ChoiceType prefreeg prefreeg_choiceMixin.
End Defs.

Implicit Arguments mkPrefreeg [G K].
Arguments mkPrefreeg [G K].

Section Quotient.
Variable G : zmodType.
Expand Down
26 changes: 13 additions & 13 deletions src/mpoly.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -937,7 +937,7 @@ Proof. by rewrite mdeg0. Qed.
End DegBoundMultinom.

Definition bm0 n b := BMultinom (bm0_proof n b).
Implicit Arguments bm0 [n b].
Arguments bm0 [n b].

Notation "''X_{1..' n < b '}'" := (bmultinom n b).
Notation "''X_{1..' n < b1 , b2 '}'" := ('X_{1..n < b1} * 'X_{1..n < b2})%type.
Expand Down Expand Up @@ -1641,7 +1641,7 @@ rewrite [X in _=X]big_uncond //= => j /memN_msupp_eq0.
by move=> ->; rewrite mulr0 freegU0.
Qed.

Implicit Arguments mpoly_mulwE [p q].
Arguments mpoly_mulwE [p q].

Lemma mpoly_mul_revwE p q kp kq : msize p <= kp -> msize q <= kq ->
p *M q = [mpoly \sum_(m : 'X_{1..n < kq, kp}) (p *M_[(m.2, m.1)] q)].
Expand All @@ -1650,7 +1650,7 @@ move=> lep leq; rewrite -pair_bigA_curry exchange_big /=.
by rewrite pair_bigA /= -mpoly_mulwE //.
Qed.

Implicit Arguments mpoly_mul_revwE [p q].
Arguments mpoly_mul_revwE [p q].

Lemma mcoeff_poly_mul p q m k : !|m| < k ->
(p *M q)@_m =
Expand Down Expand Up @@ -1713,7 +1713,7 @@ rewrite -(pair_big_dep xpredT P F) (bigID Q) /= addrC.
move/mnmP/(_ i); rewrite mnmDE=> eq; move: Nle.
by rewrite eq leq_addr.
Qed.
Implicit Arguments mcoeff_poly_mul_lin [p q m].
Arguments mcoeff_poly_mul_lin [p q m].

Local Notation mcoeff_pml := mcoeff_poly_mul_lin.

Expand All @@ -1736,7 +1736,7 @@ rewrite ltn_neqAle -subn_eq0 => /andP [ne_mhi /eqP le_mhi].
apply/negbTE/eqP/mnmP=> /(_ i); rewrite !mnmBE => /eqP.
by rewrite le_mhi subn0 (negbTE ne_mhi).
Qed.
Implicit Arguments mcoeff_poly_mul_lin_rev [p q m].
Arguments mcoeff_poly_mul_lin_rev [p q m].

Local Notation mcoeff_pmlr := mcoeff_poly_mul_lin_rev.

Expand Down Expand Up @@ -2619,7 +2619,7 @@ move=> le_pk; rewrite /mderiv (big_mksub I) /=; first last.
rewrite big_uncond //= => j /memN_msupp_eq0 ->.
by rewrite mulr0 scale0r.
Qed.
Implicit Arguments mderivwE [p i].
Arguments mderivwE [i p].

Lemma mcoeff_deriv i m p : p^`M(i)@_m = p@_(m + U_(i)) *+ (m i).+1.
Proof.
Expand Down Expand Up @@ -3006,7 +3006,7 @@ rewrite /mmap (big_mksub I) ?msupp_uniq //=; first last.
rewrite big_uncond //= => j /memN_msupp_eq0 ->.
by rewrite raddf0 mul0r.
Qed.
Implicit Arguments mmapE [p].
Arguments mmapE [p].

Lemma mmap_is_additive : additive (mmap f h).
Proof.
Expand Down Expand Up @@ -3035,7 +3035,7 @@ by rewrite mcoeffC eqxx mulr1.
Qed.
End Additive.

Implicit Arguments mmapE [f h p].
Arguments mmapE [h f p].

Section Multiplicative.
Variable h : 'I_n -> S.
Expand Down Expand Up @@ -3070,7 +3070,7 @@ Qed.
End Multiplicative.
End MPolyMorphism.

Implicit Arguments mmapE [n R S h f p].
Arguments mmapE [n R S h f p].

(* -------------------------------------------------------------------- *)
Lemma mmap1_eq n (R : ringType) (f1 f2 : 'I_n -> R) m :
Expand Down Expand Up @@ -3328,7 +3328,7 @@ Proof.
rewrite /map_mpoly; move/mmapE=> -> /=; apply/eq_bigr.
by move=> i _; rewrite mmap1_id mul_mpolyC.
Qed.
Implicit Arguments map_mpolyE [p].
Arguments map_mpolyE [p].

Lemma mcoeff_map_mpoly m p : p^f@_m = f p@_m.
Proof.
Expand Down Expand Up @@ -3688,7 +3688,7 @@ rewrite [X in _='X_[X]](reindex (fun i : 'I_n => s i)) /=.
by exists (s^-1)%g=> i _; rewrite (permK, permKV).
Qed.

Implicit Arguments msymE [p].
Arguments msymE [p].

Lemma mcoeff_sym p (s : 'S_n) m : (msym s p)@_m = p@_(m#s).
Proof.
Expand Down Expand Up @@ -3842,8 +3842,8 @@ by move/msupp_le_mlead; rewrite leNgt => /negbTE=> ->.
Qed.
End MPolySym.

Implicit Arguments inj_msym [n R].
Implicit Arguments symmetric [n R].
Arguments inj_msym [n R].
Arguments symmetric [n R].

(* -------------------------------------------------------------------- *)
Section MPolySymComp.
Expand Down
4 changes: 2 additions & 2 deletions src/ssrcomplements.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -246,8 +246,8 @@ Section BigMkSub.
Qed.
End BigMkSub.

Implicit Arguments big_sub_widen [S idx op T sT rT].
Implicit Arguments big_sub_widen [S idx op T sT rT].
Arguments big_sub_widen [S idx op T sT rT].
Arguments big_sub_widen [S idx op T sT rT].

(* -------------------------------------------------------------------- *)
Section Product.
Expand Down
2 changes: 1 addition & 1 deletion src/xfinmap.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ by rewrite /index_enum -enumT mem_enum.
Qed.
End BigFSetIncl.

Implicit Arguments big_fset_incl [R idx op T A B].
Arguments big_fset_incl [R idx op T A B].

(* -------------------------------------------------------------------- *)
Module BigEnoughFSet.
Expand Down

0 comments on commit 4bdc918

Please sign in to comment.