Adapt to math-comp/math-comp#1456

proux01 · proux01 · commit 456118c968ff · 2025-09-05T10:43:50.000+02:00
diff --git a/ecc_classic/decoding.v b/ecc_classic/decoding.v
@@ -2,7 +2,8 @@
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm.
 From mathcomp Require Import zmodp matrix vector order.
-From mathcomp Require Import lra ring mathcomp_extra Rstruct reals.
+From mathcomp.algebra_tactics Require Import lra ring.
+From mathcomp Require Import mathcomp_extra Rstruct reals.
 Require Import realType_ext ssr_ext ssralg_ext f2 bigop_ext fdist proba.
 Require Import channel_code channel binary_symmetric_channel hamming pproba.
 
diff --git a/ecc_classic/hamming_code.v b/ecc_classic/hamming_code.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm.
-From mathcomp Require Import zmodp matrix mxalgebra vector ring.
+From mathcomp Require Import zmodp matrix mxalgebra vector.
+From mathcomp.algebra_tactics Require Import ring.
 From mathcomp Require Import Rstruct reals.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext f2 linearcode natbin.
 Require Import hamming fdist proba channel channel_code decoding.
diff --git a/ecc_modern/ldpc.v b/ecc_modern/ldpc.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
-From mathcomp Require Import matrix vector ssrnum lra ring.
+From mathcomp Require Import matrix vector ssrnum.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import Rstruct reals.
 Require Import realType_ext ssr_ext ssralg_ext num_occ bigop_ext.
 Require Import fdist channel pproba f2 linearcode subgraph_partition tanner.
diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v
@@ -3,7 +3,8 @@
 From HB Require Import structures.
 Require Import Init.Wf Recdef.
 From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg ssrnum.
-From mathcomp Require Import Rstruct reals ring lra.
+From mathcomp Require Import Rstruct reals.
+From mathcomp.algebra_tactics Require Import ring lra.
 Require Import f2 subgraph_partition tanner.
 Require Import fdist channel pproba linearcode ssralg_ext.
 Require Import tanner_partition summary ldpc checksum.
diff --git a/ecc_modern/ldpc_algo_proof.v b/ecc_modern/ldpc_algo_proof.v
@@ -3,7 +3,8 @@
 From HB Require Import structures.
 Require Import Wf_nat Init.Wf Recdef.
 From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg ssrnum.
-From mathcomp Require Import Rstruct reals ring lra.
+From mathcomp Require Import Rstruct reals.
+From mathcomp.algebra_tactics Require Import ring lra.
 Require Import ssr_ext ssralg_ext bigop_ext f2.
 Require Import fdist channel pproba linearcode subgraph_partition tanner.
 Require Import tanner_partition summary ldpc checksum ldpc_algo.
diff --git a/ecc_modern/summary_tanner.v b/ecc_modern/summary_tanner.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq               *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg zmodp.
-From mathcomp Require Import matrix lra ring.
+From mathcomp Require Import matrix.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import Rstruct reals.
 Require Import ssr_ext ssralg_ext f2 summary.
 Require Import subgraph_partition tanner tanner_partition fdist channel.
diff --git a/information_theory/channel_coding_direct.v b/information_theory/channel_coding_direct.v
@@ -2,7 +2,8 @@
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix perm.
-From mathcomp Require Import archimedean lra ring.
+From mathcomp Require Import archimedean.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import mathcomp_extra boolp classical_sets reals Rstruct.
 From mathcomp Require Import exp.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
diff --git a/information_theory/conditional_divergence.v b/information_theory/conditional_divergence.v
@@ -1,6 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum matrix ring lra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
+From mathcomp.algebra_tactics Require Import ring lra.
 From mathcomp Require Import Rstruct reals exp.
 Require Import ssr_ext bigop_ext ssralg_ext realType_ext realType_ln.
 Require Import num_occ fdist proba entropy channel divergence types jtypes.
diff --git a/information_theory/entropy_convex.v b/information_theory/entropy_convex.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
-From mathcomp Require Import ring.
+From mathcomp.algebra_tactics Require Import ring.
 From mathcomp Require boolp.
 From mathcomp Require Import unstable mathcomp_extra Rstruct reals.
 From mathcomp Require Import interval_inference set_interval.
diff --git a/information_theory/error_exponent.v b/information_theory/error_exponent.v
@@ -1,6 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum lra ring.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import Rstruct reals classical_sets topology normedtype.
 From mathcomp Require Import sequences exp.
 Require Import ssr_ext bigop_ext realType_ext realType_ln fdist.
diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssrnum ssrint ssralg matrix.
-From mathcomp Require Import lra ring archimedean.
+From mathcomp.algebra_tactics Require Import lra ring
+From mathcomp Require Import archimedean.
 From mathcomp Require Import unstable mathcomp_extra Rstruct reals exp.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
 Require Import fdist proba entropy aep typ_seq channel.
diff --git a/information_theory/source_coding_fl_converse.v b/information_theory/source_coding_fl_converse.v
@@ -1,6 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum matrix lra ring.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import Rstruct reals exp.
 Require Import realType_ext realType_ln fdist proba entropy aep.
 Require Import typ_seq source_code.
diff --git a/information_theory/source_coding_fl_direct.v b/information_theory/source_coding_fl_direct.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix.
-From mathcomp Require Import archimedean lra ring.
+From mathcomp Require Import archimedean.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import Rstruct reals exp.
 Require Import ssr_ext ssralg_ext realType_ln natbin fdist.
 Require Import proba entropy aep typ_seq source_code.
diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix.
-From mathcomp Require Import archimedean lra ring.
+From mathcomp Require Import archimedean.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import unstable Rstruct reals sequences exp.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
 Require Import fdist proba entropy divergence log_sum source_code.
diff --git a/information_theory/source_coding_vl_direct.v b/information_theory/source_coding_vl_direct.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix.
-From mathcomp Require Import archimedean lra ring.
+From mathcomp Require Import archimedean.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import Rstruct reals exp.
 Require Import  ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
 Require Import fdist proba entropy aep typ_seq natbin source_code.
diff --git a/lib/derive_ext.v b/lib/derive_ext.v
@@ -1,7 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
-From mathcomp Require Import ring lra.
+From mathcomp.algebra_tactics Require Import ring lra.
 From mathcomp Require Import unstable mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import set_interval.
 From mathcomp Require Import reals Rstruct topology normedtype.
diff --git a/lib/realType_ext.v b/lib/realType_ext.v
@@ -4,7 +4,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg archimedean ssrnum ssrint.
 From mathcomp Require Import reals normedtype sequences exp.
 From mathcomp Require Import unstable mathcomp_extra boolp interval_inference.
-From mathcomp Require Import lra ring Rstruct.
+From mathcomp.algebra_tactics Require Import lra ring
+From mathcomp Require Import Rstruct.
 
 (**md**************************************************************************)
 (* # Additional definitions and lemmas about numeric types                    *)
diff --git a/probability/convex.v b/probability/convex.v
@@ -4,7 +4,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg fingroup perm matrix interval.
 From mathcomp Require Import unstable mathcomp_extra boolp classical_sets.
 From mathcomp Require Import ssrnum archimedean ereal interval_inference.
-From mathcomp Require Import ring lra reals.
+From mathcomp.algebra_tactics Require Import ring lra.
+From mathcomp Require Import reals.
 Require Import ssr_ext ssralg_ext realType_ext realType_ln fdist.
 From mathcomp Require vector.
 From mathcomp.analysis Require Import (canonicals)convex.
diff --git a/probability/convex_stone.v b/probability/convex_stone.v
@@ -1,7 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix fingroup perm.
-From mathcomp Require Import lra ring.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require boolp.
 From mathcomp Require Import unstable mathcomp_extra Rstruct reals.
 Require Import ssr_ext ssralg_ext realType_ext fdist convex.
diff --git a/probability/pinsker.v b/probability/pinsker.v
@@ -1,6 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum interval ring lra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
+From mathcomp.algebra_tactics Require Import ring lra.
 From mathcomp Require Import unstable mathcomp_extra classical_sets functions.
 From mathcomp Require Import set_interval reals Rstruct topology normedtype.
 From mathcomp Require Import sequences derive exp realfun.
diff --git a/robust/robustmean.v b/robust/robustmean.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect all_algebra.
-From mathcomp Require Import lra ring.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require boolp.
 From mathcomp Require Import mathcomp_extra Rstruct reals.
 From infotheo Require Import ssr_ext ssralg_ext bigop_ext.
diff --git a/robust/weightedmean.v b/robust/weightedmean.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
-From mathcomp Require Import lra ring.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require boolp.
 From mathcomp Require Import Rstruct reals mathcomp_extra.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
diff --git a/toy_examples/conditional_entropy.v b/toy_examples/conditional_entropy.v
@@ -1,7 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg matrix.
-From mathcomp Require Import ring lra.
+From mathcomp.algebra_tactics Require Import ring lra.
 From mathcomp Require Import Rstruct reals.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln fdist.
 Require Import proba jfdist_cond entropy.
diff --git a/toy_examples/expected_value_variance.v b/toy_examples/expected_value_variance.v
@@ -1,6 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum lra ring.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import Rstruct reals.
 Require Import fdist proba.
 
diff --git a/toy_examples/expected_value_variance_ordn.v b/toy_examples/expected_value_variance_ordn.v
@@ -1,6 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum lra ring.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp.algebra_tactics Require Import lra ring.
 From mathcomp Require Import Rstruct reals.
 Require Import realType_ext fdist proba.
 
diff --git a/toy_examples/expected_value_variance_tuple.v b/toy_examples/expected_value_variance_tuple.v
@@ -1,6 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum ring lra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp.algebra_tactics Require Import ring lra.
 From mathcomp Require Import Rstruct reals.
 Require Import realType_ext fdist proba.
 
