coq-community · Lysxia · Sep 17, 2024 · Jul 20, 2024
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,8 +1,10 @@
 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.
 
@@ -20,23 +22,23 @@
 Set Warnings "+unsupported-attributes".

 (* We use this virtually everywhere, and so use "=" for it: *)
 Infix "=" := equiv : type_scope.
 Notation "(=)" := equiv (only parsing) : mc_scope.
 Notation "( x =)" := (equiv x) (only parsing) : mc_scope.
 Notation "(= x )" := (λ y, equiv y x) (only parsing) : mc_scope.
 Notation "(≠)" := (λ x y, ¬x = y) (only parsing) : mc_scope.
 Notation "x ≠ y":= (¬x = y): type_scope.
 Notation "( x ≠)" := (λ y, x ≠ y) (only parsing) : mc_scope.
 Notation "(≠ x )" := (λ y, y ≠ x) (only parsing) : mc_scope.

 Delimit Scope mc_scope with mc. 
 Global Open Scope mc_scope.

 #[global]
 Hint Extern 2 (?x = ?x) => reflexivity.
 #[global]
 Hint Extern 2 (?x = ?y) => auto_symm.
 #[global]
 Hint Extern 2 (?x = ?y) => auto_trans.

 (* Coq sometimes uses an incorrect DefaultRelation, so we override it. *)

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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