Merge pull request #96 from proux01/mc1343

CohenCyril · web-flow · commit 08f7100127f7 · 2025-02-17T12:51:42.000+01:00
Adapt to math-comp/math-comp#1343
diff --git a/theories/abel.v b/theories/abel.v
@@ -1,3 +1,4 @@
+From Coq Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field polyrcf.

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+From Coq Require Import Setoid.`
`1`	`2`	`From HB Require Import structures.`
`2`	`3`	`From mathcomp Require Import all_ssreflect all_fingroup all_algebra.`
`3`	`4`	`From mathcomp Require Import all_solvable all_field polyrcf.`