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
pi8027 committed Mar 29, 2024
1 parent fb2ecaf commit 637133c
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.

Check failure on line 128 in refinements/examples/irred.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18) 

The reference finIdomainType was not found in the current environment.

Check failure on line 128 in refinements/examples/irred.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.17) 

The reference finIdomainType was not found in the current environment.

Check failure on line 128 in refinements/examples/irred.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16) 

The reference finIdomainType was not found in the current environment.
Variable p : {poly R}.

Definition irreducibleb :=
Expand Down

0 comments on commit 637133c

Please sign in to comment.