Skip to content

Commit

Permalink
Adapt to math-comp/math-comp#1190
Browse files Browse the repository at this point in the history
  • Loading branch information
@pi8027 @proux01
pi8027 authored and proux01 committed Mar 29, 2024
1 parent 1cb9d50 commit 5c90833
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion refinements/examples/irred.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ End fin_npoly.

Section Irreducible.

Variable R : finIntegralDomainType.
Variable R : finIdomainType.
Variable p : {poly R}.

Definition irreducibleb :=
Expand Down

0 comments on commit 5c90833

Please sign in to comment.