Merge pull request #64 from proux01/mc1456

pi8027 · web-flow · commit c2aad0162511 · 2025-09-10T15:55:02.000+02:00
Revert "Adapt to math-comp/math-comp#1448"
diff --git a/theories/ssrZ.v b/theories/ssrZ.v
@@ -1,4 +1,3 @@
-From mathcomp Require all_algebra. (* remove this line when requiring Rocq > 9.1 *)
 From Coq Require Import ZArith.
 
 From HB Require Import structures.
diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v
@@ -1,4 +1,3 @@
-From mathcomp Require all_algebra. (* remove this line when requiring Rocq > 9.1 *)
 From Coq Require Import ZArith ZifyClasses ZifyBool.
 From Coq Require Export Lia.
 
diff --git a/theories/zify_ssreflect.v b/theories/zify_ssreflect.v
@@ -1,4 +1,3 @@
-From mathcomp Require all_algebra. (* remove this line when requiring Rocq > 9.1 *)
 From Coq Require Import ZArith ZifyClasses ZifyInst ZifyBool.
 From Coq Require Export Lia.
 From Coq Require Znumtheory.

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,3 @@`
`1`		`-From mathcomp Require all_algebra. (* remove this line when requiring Rocq > 9.1 *)`
`2`	`1`	`From Coq Require Import ZArith.`
`3`	`2`
`4`	`3`	`From HB Require Import structures.`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,3 @@`
`1`		`-From mathcomp Require all_algebra. (* remove this line when requiring Rocq > 9.1 *)`
`2`	`1`	`From Coq Require Import ZArith ZifyClasses ZifyBool.`
`3`	`2`	`From Coq Require Export Lia.`
`4`	`3`