Skip to content

Commit 7e8584d

Browse files
authored
Merge pull request #107 from proux01/mc1415
Adapt to math-comp/math-comp#1415
2 parents 298ae37 + 3a8b0af commit 7e8584d

File tree

1 file changed

+7
-10
lines changed

1 file changed

+7
-10
lines changed

refinements/examples/irred.v

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,11 @@
11
From HB Require Import structures.
2-
Require Import mathcomp.ssreflect.ssreflect.
3-
From mathcomp
4-
Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
5-
From mathcomp
6-
Require Import bigop binomial finset finfun zmodp ssralg countalg finalg poly polydiv.
7-
From mathcomp
8-
Require Import perm fingroup.
9-
10-
From CoqEAL
11-
Require Import hrel pos param refinements binnat boolF2 seqpoly poly_op trivial_seq poly_div boolF2.
2+
From mathcomp Require Import ssreflect ssrfun ssrbool.
3+
From mathcomp Require Import eqtype ssrnat seq choice fintype tuple.
4+
From mathcomp Require Import bigop binomial finset finfun perm fingroup.
5+
From mathcomp Require Import zmodp ssralg countalg finalg poly polydiv.
6+
7+
From CoqEAL Require Import hrel pos param refinements binnat boolF2 seqpoly.
8+
From CoqEAL Require Import poly_op trivial_seq poly_div boolF2.
129

1310

1411
Set Implicit Arguments.

0 commit comments

Comments
 (0)