Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21611 #120

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
pi8027 merged 1 commit into from
Feb 27, 2026
Merged

Adapt to https://github.com/rocq-prover/rocq/pull/21611 #120

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/freeg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@
Unset Printing Implicit Defensive.

(* -------------------------------------------------------------------- *)
Local Notation simpm := Monoid.simpm.

Check warning on line 41 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-dev) 

Use of "Notation" keyword for abbreviations is deprecated, use

(* -------------------------------------------------------------------- *)
Reserved Notation "{ 'freeg' K / G }" (K at level 2, format "{ 'freeg' K / G }").
Expand Down Expand Up @@ -92,7 +92,7 @@
Canonical prefreeg_equiv_direct := defaultEncModRel equiv.

Definition type := {eq_quot equiv}.
Definition type_of of phant G & phant K := type.
Definition type_of & phant G & phant K := type.

Notation "{ 'freeg' K / G }" := (type_of (Phant G) (Phant K)).

Expand All @@ -115,8 +115,8 @@

HB.reexport.

Notation prefreeg := prefreeg.

Check warning on line 118 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-dev) 

Use of "Notation" keyword for abbreviations is deprecated, use
Notation fgequiv := equiv.

Check warning on line 119 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-dev) 

Use of "Notation" keyword for abbreviations is deprecated, use
Notation mkPrefreeg := mkPrefreeg.

Notation reduced := reduced.
Expand Down Expand Up @@ -569,7 +569,7 @@
Section Lift.
Context (M : lmodType R) (f : K -> M).

Lemma lift_is_additive : additive (fglift f).

Check warning on line 572 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 572 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 572 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-coq-8.20) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 572 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 572 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Reference additive is deprecated since mathcomp 2.5.0.
Proof.
elim/quotW=> [[D1 /= H1]]; elim/quotW=> [[D2 /= H2]].
unlock fglift; rewrite ?piE [_ + _]piE /lift /=.
Expand All @@ -579,11 +579,11 @@
End Lift.

(* -------------------------------------------------------------------- *)
Lemma coeff_is_additive x : additive (coeff x).

Check warning on line 582 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 582 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 582 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-coq-8.20) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 582 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 582 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Reference additive is deprecated since mathcomp 2.5.0.
Proof. exact: lift_is_additive R^o _. Qed.

#[export] HB.instance Definition _ x :=
GRing.isAdditive.Build {freeg K / R} R (coeff x)

Check warning on line 586 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.

Check warning on line 586 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.

Check warning on line 586 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-coq-8.20) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.

Check warning on line 586 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.

Check warning on line 586 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
(coeff_is_additive x).

Lemma coeff0 z : coeff z 0 = 0 . Proof. exact: raddf0. Qed.
Expand Down Expand Up @@ -826,7 +826,7 @@

Definition predeg (D : seq (int * K)) := \sum_(kx <- D) kx.1.

Lemma deg_is_additive: additive deg.

Check warning on line 829 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-coq-8.20) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 829 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.
Proof. exact: (@lift_is_additive _ K int^o). Qed.

#[export] HB.instance Definition _ :=
Expand Down
4 changes: 2 additions & 2 deletions src/monalg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
From mathcomp Require Import seq path choice finset fintype finfun.
From mathcomp Require Import tuple bigop ssralg ssrint ssrnum.

Require Import xfinmap.

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Set Implicit Arguments.
Unset Strict Implicit.
Expand Down Expand Up @@ -52,7 +52,7 @@
(M at level 98, format "{ 'mmorphism' M -> S }").

(* -------------------------------------------------------------------- *)
HB.mixin Record Choice_isMonomialDef V of Choice V := {
HB.mixin Record Choice_isMonomialDef V & Choice V := {
one : V;
mul : V -> V -> V;
mulmA : associative mul;
Expand All @@ -77,7 +77,7 @@
Local Notation "x * y" := (mmul x y) : monom_scope.

(* -------------------------------------------------------------------- *)
HB.mixin Record MonomialDef_isConomialDef V of MonomialDef V := {
HB.mixin Record MonomialDef_isConomialDef V & MonomialDef V := {
mulmC : commutative (@mul V)
}.

Expand Down
Loading