From 14d219476470ea4f3788d34a49815792408c1733 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sat, 20 Jul 2024 20:24:16 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530

---
 categories/product.v                         | 4 +++-
 implementations/NType_naturals.v             | 5 ++++-
 implementations/QType_rationals.v            | 3 ++-
 implementations/ZType_integers.v             | 4 +++-
 implementations/dyadics.v                    | 3 ++-
 implementations/fast_rationals.v             | 3 ++-
 implementations/field_of_fractions.v         | 5 +++--
 implementations/list.v                       | 3 ++-
 implementations/list_finite_set.v            | 3 ++-
 implementations/modular_ring.v               | 3 ++-
 implementations/natpair_integers.v           | 3 ++-
 implementations/nonneg_integers_naturals.v   | 3 ++-
 implementations/nonneg_semiring_elements.v   | 2 +-
 implementations/nonzero_field_elements.v     | 3 ++-
 implementations/peano_naturals.v             | 4 +++-
 implementations/positive_semiring_elements.v | 2 +-
 implementations/semiring_pairs.v             | 3 ++-
 implementations/stdlib_binary_integers.v     | 2 +-
 implementations/stdlib_rationals.v           | 7 ++++---
 interfaces/canonical_names.v                 | 4 +++-
 misc/JMrelation.v                            | 2 +-
 misc/util.v                                  | 3 ++-
 orders/dec_fields.v                          | 2 +-
 orders/integers.v                            | 3 ++-
 orders/nat_int.v                             | 3 ++-
 orders/naturals.v                            | 3 ++-
 orders/rationals.v                           | 3 ++-
 orders/rings.v                               | 3 ++-
 orders/semirings.v                           | 3 ++-
 quote/classquote.v                           | 2 +-
 theory/abs.v                                 | 3 ++-
 theory/cut_minus.v                           | 3 ++-
 theory/dec_fields.v                          | 2 +-
 theory/fields.v                              | 3 ++-
 theory/int_abs.v                             | 3 ++-
 theory/int_pow.v                             | 2 +-
 theory/int_to_nat.v                          | 3 ++-
 theory/integers.v                            | 3 ++-
 theory/nat_distance.v                        | 3 ++-
 theory/nat_pow.v                             | 3 ++-
 theory/naturals.v                            | 6 ++++--
 theory/rationals.v                           | 2 +-
 theory/ring_congruence.v                     | 3 ++-
 theory/ring_ideals.v                         | 3 ++-
 theory/rings.v                               | 4 ++--
 theory/series.v                              | 5 +++--
 theory/shiftl.v                              | 2 +-
 theory/ua_packed.v                           | 3 ++-
 theory/ua_subvariety.v                       | 2 +-
 varieties/rings.v                            | 2 +-
 50 files changed, 100 insertions(+), 56 deletions(-)

diff --git a/categories/product.v b/categories/product.v
index cffada08..04558672 100644
--- a/categories/product.v
+++ b/categories/product.v
@@ -1,5 +1,7 @@
 Require Import
-  MathClasses.interfaces.abstract_algebra Coq.Logic.ChoiceFacts MathClasses.interfaces.functors
+  MathClasses.interfaces.abstract_algebra.
+From Coq.Logic Require Import ChoiceFacts.
+Require Import MathClasses.interfaces.functors
   MathClasses.theory.categories MathClasses.categories.categories.
 
 (* Axiom dependent_functional_choice: DependentFunctionalChoice. *)
diff --git a/implementations/NType_naturals.v b/implementations/NType_naturals.v
index d470695f..100f18a6 100644
--- a/implementations/NType_naturals.v
+++ b/implementations/NType_naturals.v
@@ -1,7 +1,10 @@
 Require
   MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings.
+From Coq Require Import Setoid.
+Require Import
+  Bignums.SpecViaZ.NSig Bignums.SpecViaZ.NSigNAxioms Coq.NArith.NArith.
+From Coq Require Import ZArith Program Morphisms.
 Require Import
-  Coq.Setoids.Setoid Bignums.SpecViaZ.NSig Bignums.SpecViaZ.NSigNAxioms Coq.NArith.NArith Coq.ZArith.ZArith Coq.Program.Program Coq.Classes.Morphisms
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers
   MathClasses.interfaces.orders MathClasses.interfaces.additional_operations.
 
diff --git a/implementations/QType_rationals.v b/implementations/QType_rationals.v
index badb2787..b9922456 100644
--- a/implementations/QType_rationals.v
+++ b/implementations/QType_rationals.v
@@ -1,7 +1,8 @@
 Require
   MathClasses.theory.fields MathClasses.implementations.stdlib_rationals MathClasses.theory.int_pow.
+From Coq Require Import QArith.
 Require Import
-  Coq.QArith.QArith Bignums.SpecViaQ.QSig
+  Bignums.SpecViaQ.QSig
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
   MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations
   MathClasses.theory.rings MathClasses.theory.rationals.
diff --git a/implementations/ZType_integers.v b/implementations/ZType_integers.v
index 65d98ed1..9edff308 100644
--- a/implementations/ZType_integers.v
+++ b/implementations/ZType_integers.v
@@ -1,7 +1,9 @@
 Require
   MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings.
 Require Import
-  Bignums.SpecViaZ.ZSig Bignums.SpecViaZ.ZSigZAxioms Coq.NArith.NArith Coq.ZArith.ZArith
+  Bignums.SpecViaZ.ZSig Bignums.SpecViaZ.ZSigZAxioms Coq.NArith.NArith.
+From Coq Require Import ZArith.
+Require Import
   MathClasses.implementations.nonneg_integers_naturals MathClasses.interfaces.orders
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations.
 
diff --git a/implementations/dyadics.v b/implementations/dyadics.v
index 1ec24d25..2f2ad66d 100644
--- a/implementations/dyadics.v
+++ b/implementations/dyadics.v
@@ -3,8 +3,9 @@
    for some [Integers] implementation [Z]. These numbers form a ring and can be
    embedded into any [Rationals] implementation [Q].
 *)
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra
+  MathClasses.interfaces.abstract_algebra
   MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
   MathClasses.orders.minmax MathClasses.orders.integers MathClasses.orders.rationals
diff --git a/implementations/fast_rationals.v b/implementations/fast_rationals.v
index 7adb5062..f735d0b8 100644
--- a/implementations/fast_rationals.v
+++ b/implementations/fast_rationals.v
@@ -1,8 +1,9 @@
 Require
   MathClasses.theory.rings
   MathClasses.theory.shiftl MathClasses.theory.int_pow.
+From Coq Require Import QArith.
 Require Import
-  Coq.QArith.QArith Bignums.BigQ.BigQ
+  Bignums.BigQ.BigQ
   MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals
   MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations
   MathClasses.implementations.fast_naturals MathClasses.implementations.fast_integers MathClasses.implementations.field_of_fractions MathClasses.implementations.stdlib_rationals.
diff --git a/implementations/field_of_fractions.v b/implementations/field_of_fractions.v
index e2751a4b..5470eb5f 100644
--- a/implementations/field_of_fractions.v
+++ b/implementations/field_of_fractions.v
@@ -1,5 +1,6 @@
-Require Import 
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra 
+From Coq Require Import Ring.
+Require Import
+  MathClasses.interfaces.abstract_algebra
   MathClasses.theory.rings MathClasses.theory.dec_fields.
 
 Inductive Frac R `{Rap : Equiv R} `{Rzero : Zero R} : Type := frac { num: R; den: R; den_ne_0: den ≠ 0 }.
diff --git a/implementations/list.v b/implementations/list.v
index a8dadc75..be3b191c 100644
--- a/implementations/list.v
+++ b/implementations/list.v
@@ -1,5 +1,6 @@
+From Coq Require Import List SetoidList.
 Require Import
-  Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads.
 Import ListNotations.
 
 (* The below belongs in the stdlib *)
diff --git a/implementations/list_finite_set.v b/implementations/list_finite_set.v
index 91f2534f..744ad3e4 100644
--- a/implementations/list_finite_set.v
+++ b/implementations/list_finite_set.v
@@ -1,5 +1,6 @@
+From Coq Require Import List SetoidList.
 Require Import
-  Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list
+  MathClasses.implementations.list
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders
   MathClasses.theory.lattices MathClasses.orders.lattices.
 Import ListNotations.
diff --git a/implementations/modular_ring.v b/implementations/modular_ring.v
index b222c620..1da424c1 100644
--- a/implementations/modular_ring.v
+++ b/implementations/modular_ring.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers
   MathClasses.theory.integers MathClasses.theory.ring_ideals.
 
 Definition is_multiple `{Equiv Z} `{Mult Z} (b x : Z) := ∃ k, x = b * k.
diff --git a/implementations/natpair_integers.v b/implementations/natpair_integers.v
index 6e7e56f7..5f9f801e 100644
--- a/implementations/natpair_integers.v
+++ b/implementations/natpair_integers.v
@@ -6,8 +6,9 @@
 
 Require
  MathClasses.theory.naturals.
+From Coq Require Import Ring.
 Require Import
- Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.categories
+ MathClasses.interfaces.abstract_algebra MathClasses.theory.categories
  MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.theory.jections.
 Require Export
  MathClasses.implementations.semiring_pairs.
diff --git a/implementations/nonneg_integers_naturals.v b/implementations/nonneg_integers_naturals.v
index 2346af8d..0bca06de 100644
--- a/implementations/nonneg_integers_naturals.v
+++ b/implementations/nonneg_integers_naturals.v
@@ -1,7 +1,8 @@
 Require 
   MathClasses.implementations.peano_naturals.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.orders
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.orders
   MathClasses.interfaces.additional_operations MathClasses.theory.int_abs.
 Require Export
   MathClasses.implementations.nonneg_semiring_elements.
diff --git a/implementations/nonneg_semiring_elements.v b/implementations/nonneg_semiring_elements.v
index 84ba6af4..01bc7b55 100644
--- a/implementations/nonneg_semiring_elements.v
+++ b/implementations/nonneg_semiring_elements.v
@@ -1,7 +1,7 @@
 Require
   MathClasses.theory.rings.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.semirings.
 
 Local Existing Instance pseudo_srorder_semiring.
diff --git a/implementations/nonzero_field_elements.v b/implementations/nonzero_field_elements.v
index bb7d8c52..c4fe6321 100644
--- a/implementations/nonzero_field_elements.v
+++ b/implementations/nonzero_field_elements.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.fields.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.fields.
 
 (* The non zero elements of a field form a CommutativeMonoid. *)
 Section contents.
diff --git a/implementations/peano_naturals.v b/implementations/peano_naturals.v
index cd4eb88b..24742242 100644
--- a/implementations/peano_naturals.v
+++ b/implementations/peano_naturals.v
@@ -1,7 +1,9 @@
 Require
   MathClasses.theory.ua_homomorphisms.
 Require Import
-  Coq.Classes.Morphisms Coq.setoid_ring.Ring Coq.Arith.Arith_base Coq.Arith.PeanoNat
+  Coq.Classes.Morphisms.
+From Coq Require Import Ring Arith_base PeanoNat.
+Require Import
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.semirings.
 
diff --git a/implementations/positive_semiring_elements.v b/implementations/positive_semiring_elements.v
index 9f43a18d..54dd4fea 100644
--- a/implementations/positive_semiring_elements.v
+++ b/implementations/positive_semiring_elements.v
@@ -1,5 +1,5 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations
   MathClasses.interfaces.orders MathClasses.interfaces.integers
   MathClasses.orders.semirings MathClasses.theory.shiftl MathClasses.theory.int_pow.
diff --git a/implementations/semiring_pairs.v b/implementations/semiring_pairs.v
index beb0fd85..76008e1b 100644
--- a/implementations/semiring_pairs.v
+++ b/implementations/semiring_pairs.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings.
 
 Inductive SRpair (SR : Type) := C { pos : SR ; neg : SR }.
 Arguments C {SR} _ _.
diff --git a/implementations/stdlib_binary_integers.v b/implementations/stdlib_binary_integers.v
index 9dd71504..c362ee6c 100644
--- a/implementations/stdlib_binary_integers.v
+++ b/implementations/stdlib_binary_integers.v
@@ -1,7 +1,7 @@
 Require
   MathClasses.interfaces.naturals MathClasses.theory.naturals MathClasses.implementations.peano_naturals MathClasses.theory.integers.
+From Coq Require Import BinInt Ring Arith NArith ZArith ZBinary.
 Require Import
-  Coq.ZArith.BinInt Coq.setoid_ring.Ring Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Numbers.Integer.Binary.ZBinary
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers
   MathClasses.implementations.natpair_integers MathClasses.implementations.stdlib_binary_naturals
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
diff --git a/implementations/stdlib_rationals.v b/implementations/stdlib_rationals.v
index 5334249c..cc8c2d57 100644
--- a/implementations/stdlib_rationals.v
+++ b/implementations/stdlib_rationals.v
@@ -1,8 +1,9 @@
 Require
-  MathClasses.implementations.stdlib_binary_integers Coq.setoid_ring.Field Coq.QArith.Qfield MathClasses.theory.rationals.
+  MathClasses.implementations.stdlib_binary_integers.
+From Coq Require Import Field Qfield.
+Require Import MathClasses.theory.rationals.
+From Coq Require Import ZArith Ring QArith_base Qabs Qpower.
 Require Import
-  Coq.ZArith.ZArith
-  Coq.setoid_ring.Ring Coq.QArith.QArith_base Coq.QArith.Qabs Coq.QArith.Qpower
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.rationals
   MathClasses.interfaces.orders MathClasses.interfaces.additional_operations
   MathClasses.implementations.field_of_fractions MathClasses.orders.integers.
diff --git a/interfaces/canonical_names.v b/interfaces/canonical_names.v
index bdd34493..d287a609 100644
--- a/interfaces/canonical_names.v
+++ b/interfaces/canonical_names.v
@@ -2,7 +2,9 @@ Global Generalizable All Variables.
 Global Set Automatic Introduction.
 
 Require Import MathClasses.theory.CoqStreams.
-Require Export Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Program.Program Coq.Unicode.Utf8 Coq.Unicode.Utf8_core MathClasses.misc.stdlib_hints.
+Require Export Coq.Classes.Morphisms Coq.Setoids.Setoid.
+From Coq.Program Require Export Program.
+Require Export Coq.Unicode.Utf8 Coq.Unicode.Utf8_core MathClasses.misc.stdlib_hints.
 
 Definition id {A : Type} (a : A) := a.
 
diff --git a/misc/JMrelation.v b/misc/JMrelation.v
index 01602abf..edb3e108 100644
--- a/misc/JMrelation.v
+++ b/misc/JMrelation.v
@@ -14,7 +14,7 @@ Lemma transitive A B C (Ra: relation A) (Rb: relation B) (Rc: relation C) (a:A)
   R Ra a _ Rb b → R Rb b _ Rc c → R Ra a _ Rc c.
 Proof. destruct 1. destruct 1. apply relate. transitivity y; assumption. Qed.
 
-Require Import Coq.Logic.Eqdep.
+From Coq.Logic Require Import Eqdep.
 
 Lemma unJM A (r: relation A) (x y:A) r' (E: R r x A r' y): r x y.
 Proof.
diff --git a/misc/util.v b/misc/util.v
index d67d7779..0a502202 100644
--- a/misc/util.v
+++ b/misc/util.v
@@ -1,5 +1,6 @@
+From Coq.Program Require Import Program.
 Require Import
-  Coq.Program.Program Coq.Classes.Morphisms Coq.Setoids.Setoid MathClasses.interfaces.canonical_names.
+  Coq.Classes.Morphisms Coq.Setoids.Setoid MathClasses.interfaces.canonical_names.
 
 Section pointwise_dependent_relation.
   Context A (B: A → Type) (R: ∀ a, relation (B a)).
diff --git a/orders/dec_fields.v b/orders/dec_fields.v
index b28c3ab2..5f07069f 100644
--- a/orders/dec_fields.v
+++ b/orders/dec_fields.v
@@ -1,5 +1,5 @@
+From Coq Require Import Relation_Definitions Ring.
 Require Import
-  Coq.Relations.Relation_Definitions Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.theory.dec_fields.
 Require Export
   MathClasses.orders.rings.
diff --git a/orders/integers.v b/orders/integers.v
index c9df5c23..b3c4cd0e 100644
--- a/orders/integers.v
+++ b/orders/integers.v
@@ -1,7 +1,8 @@
 Require
   MathClasses.theory.integers MathClasses.theory.int_abs.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
   MathClasses.implementations.natpair_integers MathClasses.orders.rings.
 Require Export
diff --git a/orders/nat_int.v b/orders/nat_int.v
index 22215eb6..8eb5a521 100644
--- a/orders/nat_int.v
+++ b/orders/nat_int.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders
   MathClasses.theory.naturals MathClasses.theory.rings MathClasses.implementations.peano_naturals.
 Require Export
   MathClasses.orders.semirings.
diff --git a/orders/naturals.v b/orders/naturals.v
index be6ba7f1..c40bdf9b 100644
--- a/orders/naturals.v
+++ b/orders/naturals.v
@@ -1,7 +1,8 @@
 Require
   MathClasses.theory.naturals.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.orders.rings.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.orders.rings.
 Require Export
   MathClasses.orders.nat_int.
 
diff --git a/orders/rationals.v b/orders/rationals.v
index cab14225..7b1ece21 100644
--- a/orders/rationals.v
+++ b/orders/rationals.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring Field.
 Require Import
-  Coq.setoid_ring.Ring Coq.setoid_ring.Field MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
   MathClasses.interfaces.naturals MathClasses.interfaces.rationals MathClasses.interfaces.integers
   MathClasses.implementations.natpair_integers MathClasses.theory.rationals MathClasses.theory.dec_fields MathClasses.theory.rings
   MathClasses.orders.integers MathClasses.orders.dec_fields.
diff --git a/orders/rings.v b/orders/rings.v
index f0f5cb9e..39cf5e4b 100644
--- a/orders/rings.v
+++ b/orders/rings.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings.
 Require Export
   MathClasses.orders.semirings.
 
diff --git a/orders/semirings.v b/orders/semirings.v
index a1ce9ed4..5fd9fc6a 100644
--- a/orders/semirings.v
+++ b/orders/semirings.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings.
 Require Export
   MathClasses.orders.orders MathClasses.orders.maps.
 
diff --git a/quote/classquote.v b/quote/classquote.v
index 227c1bf1..df1e3f28 100644
--- a/quote/classquote.v
+++ b/quote/classquote.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.Morphisms Coq.Program.Program Coq.Unicode.Utf8.
+From Coq Require Import Morphisms Program Utf8.
 
 (* First, two ways to do quoting in the naive scenario without
  holes/variables in the expression: *)
diff --git a/theory/abs.v b/theory/abs.v
index 48e08cfa..a96c79f5 100644
--- a/theory/abs.v
+++ b/theory/abs.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings.
 
 Section contents.
 Context `{Ring R} `{Apart R} `{!TrivialApart R} `{!FullPseudoSemiRingOrder Rle Rlt} `{∀ x y, Decision (x = y)} `{a : !Abs R}.
diff --git a/theory/cut_minus.v b/theory/cut_minus.v
index 32e5233e..0d3fb96a 100644
--- a/theory/cut_minus.v
+++ b/theory/cut_minus.v
@@ -1,7 +1,8 @@
 Require
   MathClasses.orders.semirings.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations
   MathClasses.interfaces.orders MathClasses.orders.minmax.
 
 (* * Properties of Cut off Minus *)
diff --git a/theory/dec_fields.v b/theory/dec_fields.v
index 8f3cfa1c..76cbef1f 100644
--- a/theory/dec_fields.v
+++ b/theory/dec_fields.v
@@ -1,5 +1,5 @@
+From Coq Require Import Field Ring.
 Require Import
-  Coq.setoid_ring.Field Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace
   MathClasses.theory.fields MathClasses.theory.strong_setoids.
 Require Export
diff --git a/theory/fields.v b/theory/fields.v
index 3ec52b73..3ae7c95e 100644
--- a/theory/fields.v
+++ b/theory/fields.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids.
 Require Export
   MathClasses.theory.rings.
 
diff --git a/theory/int_abs.v b/theory/int_abs.v
index ea6c595b..f17c83dd 100644
--- a/theory/int_abs.v
+++ b/theory/int_abs.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
+  MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
   MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings.
 
 Section contents.
diff --git a/theory/int_pow.v b/theory/int_pow.v
index 20bc70d4..433eae76 100644
--- a/theory/int_pow.v
+++ b/theory/int_pow.v
@@ -1,7 +1,7 @@
 Require
   MathClasses.theory.naturals MathClasses.orders.semirings MathClasses.orders.integers MathClasses.orders.dec_fields.
+From Coq Require Import Ring Field.
 Require Import
-  Coq.setoid_ring.Ring Coq.setoid_ring.Field
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
   MathClasses.theory.nat_pow MathClasses.theory.int_abs MathClasses.theory.dec_fields.
diff --git a/theory/int_to_nat.v b/theory/int_to_nat.v
index e4251f9a..acfa7617 100644
--- a/theory/int_to_nat.v
+++ b/theory/int_to_nat.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
+  MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
   MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings.
 
 Section contents. 
diff --git a/theory/integers.v b/theory/integers.v
index 56da9f0c..51c54a94 100644
--- a/theory/integers.v
+++ b/theory/integers.v
@@ -1,8 +1,9 @@
 (* General results about arbitrary integer implementations. *)
 Require
  MathClasses.theory.nat_distance.
+From Coq Require Import Ring.
 Require Import
- Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers.
+ MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers.
 Require Export
  MathClasses.interfaces.integers.
 
diff --git a/theory/nat_distance.v b/theory/nat_distance.v
index ecc6992e..d68ad529 100644
--- a/theory/nat_distance.v
+++ b/theory/nat_distance.v
@@ -1,7 +1,8 @@
 Require
   MathClasses.orders.naturals MathClasses.implementations.peano_naturals.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations.
 
 Section contents.
 Context `{Naturals N}.
diff --git a/theory/nat_pow.v b/theory/nat_pow.v
index f6615587..54166ad9 100644
--- a/theory/nat_pow.v
+++ b/theory/nat_pow.v
@@ -1,7 +1,8 @@
 Require
   MathClasses.theory.naturals.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations.
 
 (* * Properties of Nat Pow *)
 Section nat_pow_properties.
diff --git a/theory/naturals.v b/theory/naturals.v
index 510a10fa..4f7331c9 100644
--- a/theory/naturals.v
+++ b/theory/naturals.v
@@ -1,6 +1,8 @@
+From Coq Require Import Ring.
+Require Import
+  MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings.
+From Coq Require Import PeanoNat.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings
-  Coq.Arith.PeanoNat
   MathClasses.categories.varieties MathClasses.theory.ua_transference.
 Require Export
   MathClasses.interfaces.naturals.
diff --git a/theory/rationals.v b/theory/rationals.v
index 50cf751d..17a62f42 100644
--- a/theory/rationals.v
+++ b/theory/rationals.v
@@ -1,5 +1,5 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals
   MathClasses.implementations.field_of_fractions MathClasses.implementations.natpair_integers
   MathClasses.theory.rings MathClasses.theory.integers MathClasses.theory.dec_fields.
diff --git a/theory/ring_congruence.v b/theory/ring_congruence.v
index b7743c64..7c9a9d6e 100644
--- a/theory/ring_congruence.v
+++ b/theory/ring_congruence.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.rings.
 
 Class RingCongruence A (R : relation A) `{Ring A} :=
   { ring_congr_equivalence : Equivalence R
diff --git a/theory/ring_ideals.v b/theory/ring_ideals.v
index b0853e74..d0d078a6 100644
--- a/theory/ring_ideals.v
+++ b/theory/ring_ideals.v
@@ -1,7 +1,8 @@
  (* We define what a ring ideal is, show that they yield congruences,
  define what a kernel is, and show that kernels are ideal. *)
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.rings.
 Require Export
    MathClasses.theory.ring_congruence.
 
diff --git a/theory/rings.v b/theory/rings.v
index a2647d44..ca5335e7 100644
--- a/theory/rings.v
+++ b/theory/rings.v
@@ -1,7 +1,7 @@
 Require
   MathClasses.varieties.monoids MathClasses.theory.groups MathClasses.theory.strong_setoids.
-Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra.
+From Coq Require Import Ring.
+Require Import MathClasses.interfaces.abstract_algebra.
 
 Definition is_ne_0 `(x : R) `{Equiv R} `{Zero R} `{p : PropHolds (x ≠ 0)} : x ≠ 0 := p.
 Definition is_nonneg `(x : R) `{Equiv R} `{Le R} `{Zero R} `{p : PropHolds (0 ≤ x)} : 0 ≤ x := p.
diff --git a/theory/series.v b/theory/series.v
index 05a842e5..653125ec 100644
--- a/theory/series.v
+++ b/theory/series.v
@@ -1,5 +1,6 @@
+From Coq Require Import Ring Factorial.
 Require Import
-  Coq.setoid_ring.Ring Coq.Arith.Factorial MathClasses.misc.workaround_tactics
+  MathClasses.misc.workaround_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
   MathClasses.interfaces.naturals MathClasses.interfaces.integers
   MathClasses.theory.nat_pow MathClasses.theory.int_pow MathClasses.theory.streams.
@@ -313,4 +314,4 @@ Section preservation.
     rewrite 2!Str_nth_factorials.
     now rewrite <-(naturals.to_semiring_unique (f ∘ naturals_to_semiring nat A)).
   Qed.
-End preservation.
\ No newline at end of file
+End preservation.
diff --git a/theory/shiftl.v b/theory/shiftl.v
index 1ecd5b8f..9615afad 100644
--- a/theory/shiftl.v
+++ b/theory/shiftl.v
@@ -1,7 +1,7 @@
 Require
   MathClasses.orders.integers MathClasses.theory.dec_fields MathClasses.theory.nat_pow.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders.
 
diff --git a/theory/ua_packed.v b/theory/ua_packed.v
index 4f6fd5ae..2f8551c9 100644
--- a/theory/ua_packed.v
+++ b/theory/ua_packed.v
@@ -1,5 +1,6 @@
 Require Import
-  MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra Coq.Program.Program.
+  MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra.
+From Coq Require Import Program.
 
 Section packed.
   Context (σ: Signature) {V: Type}.
diff --git a/theory/ua_subvariety.v b/theory/ua_subvariety.v
index 48045dc7..59fd001e 100644
--- a/theory/ua_subvariety.v
+++ b/theory/ua_subvariety.v
@@ -1,5 +1,5 @@
+From Coq Require Import RelationClasses Morphisms Program.
 Require Import
-  Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Program.Program
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebra.
 
 (* In theory/ua_subalgebra.v we defined closed proper subsets and showed that
diff --git a/varieties/rings.v b/varieties/rings.v
index f7e39740..8989d7e6 100644
--- a/varieties/rings.v
+++ b/varieties/rings.v
@@ -1,8 +1,8 @@
 (* To be imported qualified. *)
 Require
   MathClasses.categories.varieties MathClasses.theory.rings.
+From Coq Require Import Ring.
 Require Import
-  Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics.
 
 Inductive op := plus | mult | zero | one | negate.