Patch for trunk branch of https://gforge.inria.fr/git/coq-contribs/math-classes.git

mathclasses.patch

commit ec8f935df189b4857b064768d86591bb035b8783
Author: Jason Gross <[email protected]>
Date:   Thu May 7 16:27:10 2015 -0400

    Absolutize all [Import]s
    
    Previously, on case-insensitive file systems, Coq thought that [Require
    Import List] meant [Require Import MathClasses.implementations.List]
    (which is invalid), not [Require Import Coq.Lists.List].  This fixes
    that.
    
    This commit was fully automatic, achieved by running
    ```
    make
    git ls-files "*.v" | xargs python /path/to/coq-tools/absolutize-imports.py -R . MathClasses
    ```
    where `/path/to/coq-tools` is the path to a local clone of my [coq-tools
    repository](https://github.com/JasonGross/coq-tools).

diff --git a/categories/JMcat.v b/categories/JMcat.v
index 401fc32..3151f22 100644
--- a/categories/JMcat.v
+++ b/categories/JMcat.v
@@ -1,7 +1,7 @@
 Require
-  JMrelation.
+  MathClasses.misc.JMrelation.
 Require Import
-  abstract_algebra interfaces.functors theory.categories.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors MathClasses.theory.categories.
 
 Record Object := object
   { obj:> Type
diff --git a/categories/algebras.v b/categories/algebras.v
index 1c5046a..d381c49 100644
--- a/categories/algebras.v
+++ b/categories/algebras.v
@@ -1,8 +1,8 @@
 (* Show that algebras with homomorphisms between them form a category. *)
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms theory.categories.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories.
 Require
-  categories.setoids categories.product.
+  MathClasses.categories.setoids MathClasses.categories.product.
 
 Record Object (sign: Signature) : Type := object
   { algebra_carriers:> sorts sign → Type
diff --git a/categories/categories.v b/categories/categories.v
index df0503f..7886fa1 100644
--- a/categories/categories.v
+++ b/categories/categories.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.functors theory.categories.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors MathClasses.theory.categories.
 
 Record Object := object
   { obj:> Type
diff --git a/categories/dual.v b/categories/dual.v
index eec6808..60f0c3e 100644
--- a/categories/dual.v
+++ b/categories/dual.v
@@ -1,5 +1,5 @@
 Require Import
-  Relation_Definitions abstract_algebra theory.categories interfaces.functors.
+  Coq.Relations.Relation_Definitions MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.interfaces.functors.
 
 Section contents.
 
diff --git a/categories/empty.v b/categories/empty.v
index 5a5d40b..2a3c02e 100644
--- a/categories/empty.v
+++ b/categories/empty.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.functors.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors.
 
 Definition Empty_map {A: Empty_set → Type} : ∀ x : Empty_set, A x := λ x, match x with end.
 Local Notation E := Empty_map.
diff --git a/categories/functors.v b/categories/functors.v
index 4aa1392..8c86dbe 100644
--- a/categories/functors.v
+++ b/categories/functors.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.functors theory.categories.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors MathClasses.theory.categories.
 
 Section natural_transformations_id_comp.
   Context
diff --git a/categories/orders.v b/categories/orders.v
index 0b03b0e..41fc560 100644
--- a/categories/orders.v
+++ b/categories/orders.v
@@ -1,7 +1,7 @@
 Require Import
-  abstract_algebra theory.categories orders.maps interfaces.orders orders.orders
-  interfaces.functors.
-Require categories.setoids.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.orders.maps MathClasses.interfaces.orders MathClasses.orders.orders
+  MathClasses.interfaces.functors.
+Require MathClasses.categories.setoids.
 
 Inductive Object := object { T:> Type; e: Equiv T; le: Le T; setoid_proof: Setoid T;  po_proof: PartialOrder le }.
 Existing Instance e.
diff --git a/categories/product.v b/categories/product.v
index 65e9c81..811822b 100644
--- a/categories/product.v
+++ b/categories/product.v
@@ -1,6 +1,6 @@
 Require Import
-  abstract_algebra ChoiceFacts interfaces.functors
-  theory.categories categories.categories.
+  MathClasses.interfaces.abstract_algebra Coq.Logic.ChoiceFacts MathClasses.interfaces.functors
+  MathClasses.theory.categories MathClasses.categories.categories.
 
 (* Axiom dependent_functional_choice: DependentFunctionalChoice. *)
 
diff --git a/categories/setoids.v b/categories/setoids.v
index b63daaf..ab5f364 100644
--- a/categories/setoids.v
+++ b/categories/setoids.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra theory.categories.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.categories.
 
 Inductive Object := object { T:> Type; e: Equiv T; setoid_proof: Setoid T }.
 Arguments object _ {e setoid_proof}.
diff --git a/categories/unit.v b/categories/unit.v
index 28f8546..36a2c16 100644
--- a/categories/unit.v
+++ b/categories/unit.v
@@ -1,6 +1,6 @@
 Require Import
-  RelationClasses Equivalence
-  categories.categories abstract_algebra categories.functors.
+  Coq.Classes.RelationClasses Coq.Classes.Equivalence
+  MathClasses.categories.categories MathClasses.interfaces.abstract_algebra MathClasses.categories.functors.
 
 Instance: Arrows unit := λ _ _, unit.
 Instance: CatId unit := λ _, tt.
diff --git a/categories/varieties.v b/categories/varieties.v
index 7e9ce19..c1d0c0b 100644
--- a/categories/varieties.v
+++ b/categories/varieties.v
@@ -5,7 +5,7 @@ factor out the commonality.
 
  *)
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms.
 
 Record Object (et: EquationalTheory) : Type := object
   { variety_carriers:> sorts et → Type
diff --git a/functors/constant.v b/functors/constant.v
index 52b307a..d4766ce 100644
--- a/functors/constant.v
+++ b/functors/constant.v
@@ -1,5 +1,5 @@
 Require Import
-  theory.categories abstract_algebra interfaces.functors.
+  MathClasses.theory.categories MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors.
 
 Section constant_functor.
   Context `{Category A} `{Category B}.
diff --git a/implementations/NType_naturals.v b/implementations/NType_naturals.v
index 75a903f..10ee4a1 100644
--- a/implementations/NType_naturals.v
+++ b/implementations/NType_naturals.v
@@ -1,9 +1,9 @@
 Require
-  stdlib_binary_integers theory.integers orders.semirings.
+  MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings.
 Require Import
-  Setoid NSig NSigNAxioms NArith ZArith Program Morphisms
-  abstract_algebra interfaces.naturals interfaces.integers
-  interfaces.orders interfaces.additional_operations.
+  Coq.Setoids.Setoid Coq.Numbers.Natural.SpecViaZ.NSig Coq.Numbers.Natural.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.
 
 Module NType_Integers (Import anyN: NType).
 
diff --git a/implementations/QType_rationals.v b/implementations/QType_rationals.v
index 175f6c8..7949a57 100644
--- a/implementations/QType_rationals.v
+++ b/implementations/QType_rationals.v
@@ -1,10 +1,10 @@
 Require
-  theory.fields stdlib_rationals theory.int_pow.
+  MathClasses.theory.fields MathClasses.implementations.stdlib_rationals MathClasses.theory.int_pow.
 Require Import
-  QArith QSig
-  abstract_algebra interfaces.orders
-  interfaces.integers interfaces.rationals interfaces.additional_operations
-  theory.rings theory.rationals.
+  Coq.QArith.QArith Coq.Numbers.Rational.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.
 
 Module QType_Rationals (Import anyQ: QType).
 
diff --git a/implementations/ZType_integers.v b/implementations/ZType_integers.v
index 7052cfe..3024e21 100644
--- a/implementations/ZType_integers.v
+++ b/implementations/ZType_integers.v
@@ -1,9 +1,9 @@
 Require
-  stdlib_binary_integers theory.integers orders.semirings.
+  MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings.
 Require Import
-  ZSig ZSigZAxioms NArith ZArith
-  nonneg_integers_naturals interfaces.orders
-  abstract_algebra interfaces.integers interfaces.additional_operations.
+  Coq.Numbers.Integer.SpecViaZ.ZSig Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms Coq.NArith.NArith Coq.ZArith.ZArith
+  MathClasses.implementations.nonneg_integers_naturals MathClasses.interfaces.orders
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations.
 
 Module ZType_Integers (Import anyZ: ZType).
 
diff --git a/implementations/bool.v b/implementations/bool.v
index 330e9c0..5c19899 100644
--- a/implementations/bool.v
+++ b/implementations/bool.v
@@ -1,4 +1,4 @@
-Require Import abstract_algebra.
+Require Import MathClasses.interfaces.abstract_algebra.
 
 Instance bool_eq: Equiv bool := eq.
 Instance bool_bottom: Bottom bool := false.
diff --git a/implementations/dyadics.v b/implementations/dyadics.v
index b3c3325..c5adfe8 100644
--- a/implementations/dyadics.v
+++ b/implementations/dyadics.v
@@ -4,12 +4,12 @@
    embedded into any [Rationals] implementation [Q].
 *)
 Require Import
-  Ring abstract_algebra
-  interfaces.integers interfaces.naturals interfaces.rationals
-  interfaces.additional_operations interfaces.orders
-  orders.minmax orders.integers orders.rationals
-  nonneg_integers_naturals stdlib_rationals
-  theory.rationals theory.shiftl theory.int_pow theory.nat_pow theory.abs.
+  Coq.setoid_ring.Ring 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
+  MathClasses.implementations.nonneg_integers_naturals MathClasses.implementations.stdlib_rationals
+  MathClasses.theory.rationals MathClasses.theory.shiftl MathClasses.theory.int_pow MathClasses.theory.nat_pow MathClasses.theory.abs.
 
 Record Dyadic Z := dyadic { mant: Z; expo: Z }.
 Arguments dyadic {Z} _ _.
diff --git a/implementations/fast_integers.v b/implementations/fast_integers.v
index e269045..3308c31 100644
--- a/implementations/fast_integers.v
+++ b/implementations/fast_integers.v
@@ -1,9 +1,9 @@
 Require Import
-  BigZ
-  interfaces.abstract_algebra interfaces.integers
-  interfaces.additional_operations fast_naturals.
+  Coq.Numbers.Integer.BigZ.BigZ
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers
+  MathClasses.interfaces.additional_operations MathClasses.implementations.fast_naturals.
 Require Export
-  ZType_integers.
+  MathClasses.implementations.ZType_integers.
 
 Module BigZ_Integers := ZType_Integers BigZ.
 
diff --git a/implementations/fast_naturals.v b/implementations/fast_naturals.v
index c26cd29..77e1102 100644
--- a/implementations/fast_naturals.v
+++ b/implementations/fast_naturals.v
@@ -1,6 +1,6 @@
 Require Import
-  BigN interfaces.naturals.
+  Coq.Numbers.Natural.BigN.BigN MathClasses.interfaces.naturals.
 Require Export
-  NType_naturals.
+  MathClasses.implementations.NType_naturals.
 
 Module BigN_Integers := NType_Integers BigN.
diff --git a/implementations/fast_rationals.v b/implementations/fast_rationals.v
index 1884d7f..30492da 100644
--- a/implementations/fast_rationals.v
+++ b/implementations/fast_rationals.v
@@ -1,12 +1,12 @@
 Require
-  theory.shiftl theory.int_pow.
+  MathClasses.theory.shiftl MathClasses.theory.int_pow.
 Require Import
-  QArith BigQ
-  abstract_algebra
-  interfaces.integers interfaces.rationals interfaces.additional_operations
-  fast_naturals fast_integers field_of_fractions stdlib_rationals.
+  Coq.QArith.QArith Coq.Numbers.Rational.BigQ.BigQ
+  MathClasses.interfaces.abstract_algebra
+  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.
 Require Export
-  QType_rationals.
+  MathClasses.implementations.QType_rationals.
 
 Module Import BigQ_Rationals := QType_Rationals BigQ.
 
diff --git a/implementations/field_of_fractions.v b/implementations/field_of_fractions.v
index 647861c..8ec46e6 100644
--- a/implementations/field_of_fractions.v
+++ b/implementations/field_of_fractions.v
@@ -1,6 +1,6 @@
 Require Import 
-  Ring abstract_algebra 
-  theory.rings theory.dec_fields.
+  Coq.setoid_ring.Ring 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 }.
   (* We used to have [den] and [den_nonzero] bundled, which did work relatively nicely with Program, but the
diff --git a/implementations/intfrac_rationals.v b/implementations/intfrac_rationals.v
index f8ca716..0de4ed1 100644
--- a/implementations/intfrac_rationals.v
+++ b/implementations/intfrac_rationals.v
@@ -1,8 +1,8 @@
 Require Import
-  interfaces.rationals interfaces.integers
-  abstract_algebra theory.rationals.
+  MathClasses.interfaces.rationals MathClasses.interfaces.integers
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.rationals.
 Require Export
-  field_of_fractions.
+  MathClasses.implementations.field_of_fractions.
 
 Section intfrac_rationals.
   Context `{Integers Z}.
diff --git a/implementations/list.v b/implementations/list.v
index b910182..2e13b3a 100644
--- a/implementations/list.v
+++ b/implementations/list.v
@@ -1,5 +1,5 @@
 Require Import
-  List SetoidList abstract_algebra interfaces.monads theory.monads.
+  Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads.
 
 (* The below belongs in the stdlib *)
 Section equivlistA_misc.
diff --git a/implementations/list_finite_set.v b/implementations/list_finite_set.v
index c27b705..6f7ce24 100644
--- a/implementations/list_finite_set.v
+++ b/implementations/list_finite_set.v
@@ -1,7 +1,7 @@
 Require Import
-  List SetoidList implementations.list
-  abstract_algebra interfaces.finite_sets interfaces.orders
-  theory.lattices orders.lattices.
+  Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders
+  MathClasses.theory.lattices MathClasses.orders.lattices.
 
 (*
 We define finite sets as unordered lists. This implementation is slow,
diff --git a/implementations/modular_ring.v b/implementations/modular_ring.v
index d9cc211..283b807 100644
--- a/implementations/modular_ring.v
+++ b/implementations/modular_ring.v
@@ -1,6 +1,6 @@
 Require Import
-  Ring abstract_algebra interfaces.integers
-  theory.integers theory.ring_ideals.
+  Coq.setoid_ring.Ring 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.
 Notation Mod b := (Factor _ (is_multiple b)).
diff --git a/implementations/mset_finite_set.v b/implementations/mset_finite_set.v
index e193fe0..60a954a 100644
--- a/implementations/mset_finite_set.v
+++ b/implementations/mset_finite_set.v
@@ -1,7 +1,7 @@
 Require Import
-  MSetInterface MSetFacts MSetProperties
-  implementations.list implementations.list_finite_set theory.finite_sets
-  interfaces.finite_sets interfaces.orders abstract_algebra.
+  Coq.MSets.MSetInterface Coq.MSets.MSetFacts Coq.MSets.MSetProperties
+  MathClasses.implementations.list MathClasses.implementations.list_finite_set MathClasses.theory.finite_sets
+  MathClasses.interfaces.finite_sets MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra.
 
 Module MSet_FSet (E : DecidableType) (Import set : WSetsOn E).
 
diff --git a/implementations/natpair_integers.v b/implementations/natpair_integers.v
index 430d111..5f09169 100644
--- a/implementations/natpair_integers.v
+++ b/implementations/natpair_integers.v
@@ -5,12 +5,12 @@
   of these integers. *)
 
 Require
- theory.naturals.
+ MathClasses.theory.naturals.
 Require Import
- Ring abstract_algebra theory.categories
- interfaces.naturals interfaces.integers jections.
+ Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.categories
+ MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.theory.jections.
 Require Export
- implementations.semiring_pairs.
+ MathClasses.implementations.semiring_pairs.
 
 Section contents.
 Context `{Naturals N}.
diff --git a/implementations/ne_list.v b/implementations/ne_list.v
index 4a8f13e..1b6f1ee 100644
--- a/implementations/ne_list.v
+++ b/implementations/ne_list.v
@@ -1,7 +1,7 @@
 (** This module should be [Require]d but not [Import]ed (except for the notations submodule). *)
 
 Require Import
-  Unicode.Utf8 Coq.Lists.List Setoid Morphisms Permutation.
+  Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation.
 
 Instance: ∀ A, Proper (@Permutation A ==> eq) (@length A).
 Proof Permutation_length.
diff --git a/implementations/nonneg_integers_naturals.v b/implementations/nonneg_integers_naturals.v
index cb35abb..761fb61 100644
--- a/implementations/nonneg_integers_naturals.v
+++ b/implementations/nonneg_integers_naturals.v
@@ -1,10 +1,10 @@
 Require 
-  peano_naturals.
+  MathClasses.implementations.peano_naturals.
 Require Import
-  Ring abstract_algebra interfaces.integers interfaces.naturals interfaces.orders
-  interfaces.additional_operations int_abs.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.orders
+  MathClasses.interfaces.additional_operations MathClasses.theory.int_abs.
 Require Export
-  implementations.nonneg_semiring_elements.
+  MathClasses.implementations.nonneg_semiring_elements.
 
 Section nonneg_integers_naturals.
 Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt}.
diff --git a/implementations/nonneg_semiring_elements.v b/implementations/nonneg_semiring_elements.v
index dfd4b60..7fd6430 100644
--- a/implementations/nonneg_semiring_elements.v
+++ b/implementations/nonneg_semiring_elements.v
@@ -1,8 +1,8 @@
 Require
-  theory.rings.
+  MathClasses.theory.rings.
 Require Import
-  Ring
-  abstract_algebra interfaces.orders orders.semirings.
+  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 44f94ac..bb7d8c5 100644
--- a/implementations/nonzero_field_elements.v
+++ b/implementations/nonzero_field_elements.v
@@ -1,5 +1,5 @@
 Require Import
-  Ring abstract_algebra theory.fields.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.fields.
 
 (* The non zero elements of a field form a CommutativeMonoid. *)
 Section contents.
diff --git a/implementations/option.v b/implementations/option.v
index 77b1956..4c819ca 100644
--- a/implementations/option.v
+++ b/implementations/option.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.monads jections theory.monads.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads.
 
 Inductive option_equiv A `{Equiv A} : Equiv (option A) :=
   | option_equiv_Some : Proper ((=) ==> (=)) Some
diff --git a/implementations/peano_naturals.v b/implementations/peano_naturals.v
index 2e46c1f..f184d51 100644
--- a/implementations/peano_naturals.v
+++ b/implementations/peano_naturals.v
@@ -1,9 +1,9 @@
 Require
-  ua_homomorphisms.
+  MathClasses.theory.ua_homomorphisms.
 Require Import
-  Morphisms Ring Arith_base
-  abstract_algebra interfaces.naturals theory.categories
-  interfaces.additional_operations interfaces.orders orders.semirings.
+  Coq.Classes.Morphisms Coq.setoid_ring.Ring Coq.Arith.Arith_base
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories
+  MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.semirings.
 
 Instance nat_equiv: Equiv nat := eq.
 Instance nat_plus: Plus nat := Peano.plus.
diff --git a/implementations/polynomials.v b/implementations/polynomials.v
index a812f06..5e163c9 100644
--- a/implementations/polynomials.v
+++ b/implementations/polynomials.v
@@ -1,6 +1,6 @@
 Require Import
-  List
-  abstract_algebra.
+  Coq.Lists.List
+  MathClasses.interfaces.abstract_algebra.
 
 Section contents.
   Context R `{Ring R}.
diff --git a/implementations/positive_semiring_elements.v b/implementations/positive_semiring_elements.v
index 58be82a..9f43a18 100644
--- a/implementations/positive_semiring_elements.v
+++ b/implementations/positive_semiring_elements.v
@@ -1,8 +1,8 @@
 Require Import
-  Ring
-  abstract_algebra additional_operations
-  interfaces.orders interfaces.integers
-  orders.semirings theory.shiftl theory.int_pow.
+  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.
 
 Local Existing Instance pseudo_srorder_semiring.
 
diff --git a/implementations/semiring_pairs.v b/implementations/semiring_pairs.v
index 22ed364..43e7907 100644
--- a/implementations/semiring_pairs.v
+++ b/implementations/semiring_pairs.v
@@ -1,5 +1,5 @@
 Require Import
-  Ring abstract_algebra interfaces.orders orders.rings.
+  Coq.setoid_ring.Ring 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 6fc290a..81f83d2 100644
--- a/implementations/stdlib_binary_integers.v
+++ b/implementations/stdlib_binary_integers.v
@@ -1,11 +1,11 @@
 Require
-  interfaces.naturals theory.naturals peano_naturals theory.integers.
+  MathClasses.interfaces.naturals MathClasses.theory.naturals MathClasses.implementations.peano_naturals MathClasses.theory.integers.
 Require Import
-  BinInt Ring Arith NArith ZArith ZBinary
-  abstract_algebra interfaces.integers
-  natpair_integers stdlib_binary_naturals
-  interfaces.additional_operations interfaces.orders
-  nonneg_integers_naturals.
+  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
+  MathClasses.implementations.nonneg_integers_naturals.
 
 (* canonical names: *)
 Instance Z_equiv: Equiv Z := eq.
diff --git a/implementations/stdlib_binary_naturals.v b/implementations/stdlib_binary_naturals.v
index 7ef5c92..2a44de3 100644
--- a/implementations/stdlib_binary_naturals.v
+++ b/implementations/stdlib_binary_naturals.v
@@ -1,7 +1,7 @@
 Require Import
-  NArith peano_naturals theory.naturals
-  abstract_algebra interfaces.naturals interfaces.orders
-  interfaces.additional_operations.  
+  Coq.NArith.NArith MathClasses.implementations.peano_naturals MathClasses.theory.naturals
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders
+  MathClasses.interfaces.additional_operations.  
 
 (* canonical names for relations/operations/constants: *)
 Instance N_equiv : Equiv N := eq.
diff --git a/implementations/stdlib_rationals.v b/implementations/stdlib_rationals.v
index c049829..2b4c0a8 100644
--- a/implementations/stdlib_rationals.v
+++ b/implementations/stdlib_rationals.v
@@ -1,10 +1,10 @@
 Require
-  stdlib_binary_integers Field QArith.Qfield theory.rationals.
+  MathClasses.implementations.stdlib_binary_integers Coq.setoid_ring.Field Coq.QArith.Qfield MathClasses.theory.rationals.
 Require Import
-  Ring QArith_base Qabs Qpower
-  abstract_algebra interfaces.rationals
-  interfaces.orders interfaces.additional_operations
-  field_of_fractions orders.integers.
+  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.
 
 (* canonical names for relations/operations/constants: *)
 Instance Q_eq: Equiv Q := Qeq.
diff --git a/interfaces/abstract_algebra.v b/interfaces/abstract_algebra.v
index fce57d9..c297cd5 100644
--- a/interfaces/abstract_algebra.v
+++ b/interfaces/abstract_algebra.v
@@ -1,5 +1,5 @@
 Require Export
-  canonical_names util decision propholds workarounds setoid_tactics.
+  MathClasses.interfaces.canonical_names MathClasses.misc.util MathClasses.misc.decision MathClasses.misc.propholds MathClasses.misc.workarounds MathClasses.misc.setoid_tactics.
 
 (* 
 For various structures we omit declaration of substructures. For example, if we 
diff --git a/interfaces/additional_operations.v b/interfaces/additional_operations.v
index 225bd2d..9a47bd3 100644
--- a/interfaces/additional_operations.v
+++ b/interfaces/additional_operations.v
@@ -1,5 +1,5 @@
 Require Import
-  Morphisms abstract_algebra.
+  Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra.
 
 Class Pow A B := pow : A → B → A.
 Infix "^" := pow : mc_scope.
diff --git a/interfaces/canonical_names.v b/interfaces/canonical_names.v
index 8946626..97f8097 100644
--- a/interfaces/canonical_names.v
+++ b/interfaces/canonical_names.v
@@ -2,8 +2,8 @@ Global Generalizable All Variables.
 Global Set Automatic Introduction.
 Global Set Automatic Coercions Import.
 
-Require Import Streams.
-Require Export Morphisms Setoid Program Unicode.Utf8 Utf8_core stdlib_hints.
+Require Import Coq.Lists.Streams.
+Require Export Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Program.Program Coq.Unicode.Utf8 Coq.Unicode.Utf8_core MathClasses.misc.stdlib_hints.
 
 Definition id {A : Type} (a : A) := a.
 
diff --git a/interfaces/finite_sets.v b/interfaces/finite_sets.v
index 4df238c..2cda57e 100644
--- a/interfaces/finite_sets.v
+++ b/interfaces/finite_sets.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.orders.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders.
 
 (*
 We define finite sets as the initial join semi lattice over a decidable type.
diff --git a/interfaces/functors.v b/interfaces/functors.v
index 1039b4c..4d490b5 100644
--- a/interfaces/functors.v
+++ b/interfaces/functors.v
@@ -1,7 +1,7 @@
 Require Import
-  abstract_algebra.
+  MathClasses.interfaces.abstract_algebra.
 Require 
-  theory.setoids.
+  MathClasses.theory.setoids.
 
 Section functor_class.
   Context `{Category C} `{Category D} (M: C → D).
diff --git a/interfaces/integers.v b/interfaces/integers.v
index 4660380..87ff778 100644
--- a/interfaces/integers.v
+++ b/interfaces/integers.v
@@ -1,8 +1,8 @@
 Require Import
-  abstract_algebra interfaces.naturals theory.categories
-  categories.varieties.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories
+  MathClasses.categories.varieties.
 Require
-  varieties.rings.
+  MathClasses.varieties.rings.
 
 Section initial_maps.
   Variable A : Type.
diff --git a/interfaces/monads.v b/interfaces/monads.v
index ec337ad..f6b637a 100644
--- a/interfaces/monads.v
+++ b/interfaces/monads.v
@@ -1,7 +1,7 @@
 Require Import
-  abstract_algebra canonical_names.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names.
 Require Export
-  interfaces.functors.
+  MathClasses.interfaces.functors.
 
 Section ops.
   Context (M : Type → Type).
diff --git a/interfaces/naturals.v b/interfaces/naturals.v
index 14d22c6..f0d88dc 100644
--- a/interfaces/naturals.v
+++ b/interfaces/naturals.v
@@ -1,6 +1,6 @@
 Require Import
- abstract_algebra theory.categories
- varieties.semirings categories.varieties.
+ MathClasses.interfaces.abstract_algebra MathClasses.theory.categories
+ MathClasses.varieties.semirings MathClasses.categories.varieties.
 
 Module bad.
   Class Naturals (A: semirings.Object) `{!InitialArrow A}: Prop :=
diff --git a/interfaces/orders.v b/interfaces/orders.v
index b587409..4761777 100644
--- a/interfaces/orders.v
+++ b/interfaces/orders.v
@@ -1,4 +1,4 @@
-Require Import abstract_algebra.
+Require Import MathClasses.interfaces.abstract_algebra.
 
 (*
 In this file we describe interfaces for ordered structures. Since we are in a
diff --git a/interfaces/rationals.v b/interfaces/rationals.v
index f767507..3298895 100644
--- a/interfaces/rationals.v
+++ b/interfaces/rationals.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.integers field_of_fractions theory.integers.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.implementations.field_of_fractions MathClasses.theory.integers.
 
 Section rationals_to_frac.
   Context (A : Type).
diff --git a/interfaces/sequences.v b/interfaces/sequences.v
index a2fbed5..d764ebc 100644
--- a/interfaces/sequences.v
+++ b/interfaces/sequences.v
@@ -1,10 +1,10 @@
 Require Import
-  List abstract_algebra theory.categories forget_algebra forget_variety
-  theory.rings interfaces.universal_algebra interfaces.functors
-  categories.setoids categories.varieties.
+  Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.theory.forget_algebra MathClasses.theory.forget_variety
+  MathClasses.theory.rings MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors
+  MathClasses.categories.setoids MathClasses.categories.varieties.
 Require
-  categories.product varieties.monoids categories.algebras
-  categories.categories theory.setoids.
+  MathClasses.categories.product MathClasses.varieties.monoids MathClasses.categories.algebras
+  MathClasses.categories.categories MathClasses.theory.setoids.
 
 Module ua := universal_algebra.
 
diff --git a/interfaces/ua_basic.v b/interfaces/ua_basic.v
index 1e2189b..8c322f3 100644
--- a/interfaces/ua_basic.v
+++ b/interfaces/ua_basic.v
@@ -1,7 +1,7 @@
 Require
-  ne_list.
+  MathClasses.implementations.ne_list.
 Require Import
-  List abstract_algebra.
+  Coq.Lists.List MathClasses.interfaces.abstract_algebra.
 
 Local Notation ne_list := ne_list.L.
 
diff --git a/interfaces/universal_algebra.v b/interfaces/universal_algebra.v
index bd5c326..b3c11e2 100644
--- a/interfaces/universal_algebra.v
+++ b/interfaces/universal_algebra.v
@@ -1,10 +1,10 @@
 Require
-  theory.setoids ne_list.
+  MathClasses.theory.setoids MathClasses.implementations.ne_list.
 Require Import
-  List
-  abstract_algebra util jections.
+  Coq.Lists.List
+  MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections.
 Require Export
-  ua_basic.
+  MathClasses.interfaces.ua_basic.
 
 Section for_signature.
   Variable σ: Signature.
diff --git a/interfaces/vectorspace.v b/interfaces/vectorspace.v
index c630ca8..ed5abf4 100644
--- a/interfaces/vectorspace.v
+++ b/interfaces/vectorspace.v
@@ -1,5 +1,5 @@
 Require Import 
-  abstract_algebra interfaces.orders.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders.
 
 (** Scalar multiplication function class *)
 Class ScalarMult K V := scalar_mult: K → V → V.
diff --git a/misc/JMrelation.v b/misc/JMrelation.v
index 05e5af3..cdbf3b1 100644
--- a/misc/JMrelation.v
+++ b/misc/JMrelation.v
@@ -1,6 +1,6 @@
 (* JMeq without the [eq] hard-wiring. Meant for use with [Require] only, not [Import]. *)
-Require Import Relation_Definitions Setoid.
-Require Export Unicode.Utf8 Utf8_core.
+Require Import Coq.Relations.Relation_Definitions Coq.Setoids.Setoid.
+Require Export Coq.Unicode.Utf8 Coq.Unicode.Utf8_core.
 
 Inductive R {A: Type} (r: relation A) (x: A): forall B: Type, relation B → B → Prop := relate y: r x y → R r x A r y.
 
@@ -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 Eqdep.
+Require Import Coq.Logic.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/benchmarks_nobuild.v b/misc/benchmarks_nobuild.v
index 788f682..eb53eba 100644
--- a/misc/benchmarks_nobuild.v
+++ b/misc/benchmarks_nobuild.v
@@ -1,6 +1,6 @@
 Require Import
-  abstract_algebra interfaces.integers interfaces.additional_operations
-  implementations.dyadics fast_integers.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations
+  MathClasses.implementations.dyadics MathClasses.implementations.fast_integers.
 
 Section wolfram_sqrt.
 Context `{Integers Z} `{!RingOrder oZ} `{!TotalOrder oZ}
diff --git a/misc/decision.v b/misc/decision.v
index cf7ff58..e135712 100644
--- a/misc/decision.v
+++ b/misc/decision.v
@@ -1,5 +1,5 @@
 Require Import
-  canonical_names util.
+  MathClasses.interfaces.canonical_names MathClasses.misc.util.
 
 Class Decision P := decide: sumbool P (¬P).
 Arguments decide _ {Decision}.
diff --git a/misc/propholds.v b/misc/propholds.v
index dc8fb7a..c215863 100644
--- a/misc/propholds.v
+++ b/misc/propholds.v
@@ -1,5 +1,5 @@
 Require Import
-  canonical_names.
+  MathClasses.interfaces.canonical_names.
 
 (*
   The following class is nice to parametrize instances by additional properties, for example:
diff --git a/misc/setoid_tactics.v b/misc/setoid_tactics.v
index 96c6dc9..e9a309a 100644
--- a/misc/setoid_tactics.v
+++ b/misc/setoid_tactics.v
@@ -1,4 +1,4 @@
-Require Import Setoid canonical_names.
+Require Import Coq.Setoids.Setoid MathClasses.interfaces.canonical_names.
 
 (*
 When math-classes is used as part of another development setoid_replace
diff --git a/misc/stdlib_hints.v b/misc/stdlib_hints.v
index 0f28950..3358804 100644
--- a/misc/stdlib_hints.v
+++ b/misc/stdlib_hints.v
@@ -1,5 +1,5 @@
-Require Import Setoid Morphisms RelationClasses.
-Require Import Utf8.
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.RelationClasses.
+Require Import Coq.Unicode.Utf8.
 
 Hint Unfold Proper respectful.
 
diff --git a/misc/util.v b/misc/util.v
index 9d99a8e..d67d777 100644
--- a/misc/util.v
+++ b/misc/util.v
@@ -1,5 +1,5 @@
 Require Import
-  Program Morphisms Setoid canonical_names.
+  Coq.Program.Program 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/misc/workarounds.v b/misc/workarounds.v
index fce33c5..2910c56 100644
--- a/misc/workarounds.v
+++ b/misc/workarounds.v
@@ -1,5 +1,5 @@
-Require Import canonical_names.
-Require Import Equivalence Morphisms RelationClasses.
+Require Import MathClasses.interfaces.canonical_names.
+Require Import Coq.Classes.Equivalence Coq.Classes.Morphisms Coq.Classes.RelationClasses.
 
 (* Remove some duplicate / obsolete instances *)
 Remove Hints Equivalence_Reflexive
diff --git a/orders/dec_fields.v b/orders/dec_fields.v
index 2e31aa1..79a4e5c 100644
--- a/orders/dec_fields.v
+++ b/orders/dec_fields.v
@@ -1,8 +1,8 @@
 Require Import
-  Relation_Definitions Ring
-  abstract_algebra interfaces.orders theory.rings theory.dec_fields.
+  Coq.Relations.Relation_Definitions Coq.setoid_ring.Ring
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.theory.dec_fields.
 Require Export
-  orders.rings.
+  MathClasses.orders.rings.
 
 Section contents.
 Context `{DecField F} `{Apart F} `{!TrivialApart F} `{!FullPseudoSemiRingOrder Fle Flt} `{∀ x y : F, Decision (x = y)}.
diff --git a/orders/integers.v b/orders/integers.v
index 236a542..d53c777 100644
--- a/orders/integers.v
+++ b/orders/integers.v
@@ -1,11 +1,11 @@
 Require
-  theory.integers theory.int_abs.
+  MathClasses.theory.integers MathClasses.theory.int_abs.
 Require Import
-  Ring abstract_algebra interfaces.integers interfaces.naturals
-  interfaces.additional_operations interfaces.orders
-  natpair_integers orders.rings.
+  Coq.setoid_ring.Ring 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
-  orders.nat_int.
+  MathClasses.orders.nat_int.
 
 Section integers.
 Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt}.
diff --git a/orders/lattices.v b/orders/lattices.v
index 50c4261..8ac47e6 100644
--- a/orders/lattices.v
+++ b/orders/lattices.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.orders orders.maps theory.lattices.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices.
 
 (*
 We prove that the algebraic definition of a lattice corresponds to the
diff --git a/orders/maps.v b/orders/maps.v
index ebbd170..d7bee98 100644
--- a/orders/maps.v
+++ b/orders/maps.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.orders orders.orders theory.setoids theory.strong_setoids.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids.
 
 Local Existing Instance order_morphism_po_a.
 Local Existing Instance order_morphism_po_b.
diff --git a/orders/minmax.v b/orders/minmax.v
index f9f1976..01df5c1 100644
--- a/orders/minmax.v
+++ b/orders/minmax.v
@@ -1,6 +1,6 @@
 Require Import
-  abstract_algebra interfaces.orders orders.orders
-  orders.lattices theory.setoids.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders
+  MathClasses.orders.lattices MathClasses.theory.setoids.
 
 Section contents.
   Context `{TotalOrder A} `{∀ x y: A, Decision (x ≤ y)}.
diff --git a/orders/nat_int.v b/orders/nat_int.v
index e2c45ca..b6e75c6 100644
--- a/orders/nat_int.v
+++ b/orders/nat_int.v
@@ -1,8 +1,8 @@
 Require Import
-  Ring abstract_algebra interfaces.naturals interfaces.orders
-  theory.naturals theory.rings peano_naturals.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders
+  MathClasses.theory.naturals MathClasses.theory.rings MathClasses.implementations.peano_naturals.
 Require Export
-  orders.semirings.
+  MathClasses.orders.semirings.
 
 (*
 We axiomatize the order on the naturals and the integers as a non trivial
diff --git a/orders/naturals.v b/orders/naturals.v
index 67063f4..ff083ef 100644
--- a/orders/naturals.v
+++ b/orders/naturals.v
@@ -1,9 +1,9 @@
 Require
-  theory.naturals.
+  MathClasses.theory.naturals.
 Require Import
-  Ring abstract_algebra interfaces.naturals interfaces.orders orders.rings.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.orders.rings.
 Require Export
-  orders.nat_int.
+  MathClasses.orders.nat_int.
 
 Section naturals_order.
 Context `{Naturals N} `{Apart N} `{!TrivialApart N} `{!FullPseudoSemiRingOrder Nle Nlt}.
diff --git a/orders/orders.v b/orders/orders.v
index 21315bf..67a7701 100644
--- a/orders/orders.v
+++ b/orders/orders.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.orders strong_setoids.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids.
 
 Lemma le_flip `{Le A} `{!TotalRelation (≤)} x y : ¬y ≤ x → x ≤ y.
 Proof. firstorder. Qed.
diff --git a/orders/rationals.v b/orders/rationals.v
index a54be86..b28f16d 100644
--- a/orders/rationals.v
+++ b/orders/rationals.v
@@ -1,8 +1,8 @@
 Require Import
-  Ring Field abstract_algebra interfaces.orders
-  interfaces.naturals interfaces.rationals interfaces.integers
-  natpair_integers theory.rationals theory.dec_fields theory.rings
-  orders.integers orders.dec_fields.
+  Coq.setoid_ring.Ring Coq.setoid_ring.Field 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.
 
 Section rationals_and_integers.
   Context `{Rationals Q} `{!SemiRingOrder Qle}
diff --git a/orders/rings.v b/orders/rings.v
index 5705976..f0f5cb9 100644
--- a/orders/rings.v
+++ b/orders/rings.v
@@ -1,7 +1,7 @@
 Require Import
-  Ring abstract_algebra interfaces.orders theory.rings.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings.
 Require Export
-  orders.semirings.
+  MathClasses.orders.semirings.
 
 Section from_ring_order.
   Context `{Ring R} `{!PartialOrder Rle}
diff --git a/orders/semirings.v b/orders/semirings.v
index e7d3640..169d8d2 100644
--- a/orders/semirings.v
+++ b/orders/semirings.v
@@ -1,7 +1,7 @@
 Require Import
-  Ring abstract_algebra interfaces.orders theory.rings.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings.
 Require Export
-  orders.orders orders.maps.
+  MathClasses.orders.orders MathClasses.orders.maps.
 
 Local Existing Instance srorder_semiring.
 Local Existing Instance strict_srorder_semiring.
diff --git a/quote/classquote.v b/quote/classquote.v
index 0fd83af..d89e684 100644
--- a/quote/classquote.v
+++ b/quote/classquote.v
@@ -1,4 +1,4 @@
-Require Import Morphisms Program Unicode.Utf8.
+Require Import Coq.Classes.Morphisms Coq.Program.Program Coq.Unicode.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 b7aa413..c5f92bb 100644
--- a/theory/abs.v
+++ b/theory/abs.v
@@ -1,5 +1,5 @@
 Require Import
-  Ring abstract_algebra interfaces.orders orders.rings.
+  Coq.setoid_ring.Ring 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/adjunctions.v b/theory/adjunctions.v
index 42f1a6f..0f360ba 100644
--- a/theory/adjunctions.v
+++ b/theory/adjunctions.v
@@ -1,8 +1,8 @@
 (** We prove the equivalence of the two definitions of adjunction. *)
 Require Import
-  abstract_algebra theory.setoids interfaces.functors theory.categories
-  workaround_tactics theory.jections.
-Require dual.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories
+  MathClasses.misc.workaround_tactics MathClasses.theory.jections.
+Require MathClasses.categories.dual.
 
 Local Hint Unfold id compose: typeclass_instances. (* todo: move *)
 Local Existing Instance injective_mor.
diff --git a/theory/categories.v b/theory/categories.v
index ea921cb..89ea54a 100644
--- a/theory/categories.v
+++ b/theory/categories.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra theory.setoids interfaces.functors theory.jections.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.jections.
 
 Notation "x ⇛ y" := (∀ a, x a ⟶ y a) (at level 90, right associativity) : mc_scope.
   (* Transformations (polymorphic arrows). Couldn't find an "arrow with dot over it" unicode character. *)
diff --git a/theory/cut_minus.v b/theory/cut_minus.v
index af83757..8ff0f70 100644
--- a/theory/cut_minus.v
+++ b/theory/cut_minus.v
@@ -1,8 +1,8 @@
 Require
-  orders.semirings.
+  MathClasses.orders.semirings.
 Require Import
-  Ring abstract_algebra interfaces.additional_operations
-  interfaces.orders orders.minmax.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations
+  MathClasses.interfaces.orders MathClasses.orders.minmax.
 
 (* * Properties of Cut off Minus *)
 Section cut_minus_properties.
diff --git a/theory/dec_fields.v b/theory/dec_fields.v
index fc59101..5ada5df 100644
--- a/theory/dec_fields.v
+++ b/theory/dec_fields.v
@@ -1,8 +1,8 @@
 Require Import
-  Field Ring
-  abstract_algebra theory.fields theory.strong_setoids.
+  Coq.setoid_ring.Field Coq.setoid_ring.Ring
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.fields MathClasses.theory.strong_setoids.
 Require Export
-  theory.rings.
+  MathClasses.theory.rings.
 
 Section contents.
 Context `{DecField F} `{∀ x y: F, Decision (x = y)}.
diff --git a/theory/fields.v b/theory/fields.v
index e9072c5..3530665 100644
--- a/theory/fields.v
+++ b/theory/fields.v
@@ -1,7 +1,7 @@
 Require Import
-  Ring abstract_algebra strong_setoids.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids.
 Require Export
-  theory.rings.
+  MathClasses.theory.rings.
 
 Section field_properties.
 Context `{Field F}.
diff --git a/theory/finite_sets.v b/theory/finite_sets.v
index c33a690..a7bb915 100644
--- a/theory/finite_sets.v
+++ b/theory/finite_sets.v
@@ -1,7 +1,7 @@
 Require Import
-  theory.lattices varieties.monoids implementations.bool
-  implementations.list_finite_set orders.lattices
-  abstract_algebra interfaces.finite_sets interfaces.orders.
+  MathClasses.theory.lattices MathClasses.varieties.monoids MathClasses.implementations.bool
+  MathClasses.implementations.list_finite_set MathClasses.orders.lattices
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders.
 
 Definition fset_car_setoid A `{FSet A} : Setoid A := setoidmor_a singleton.
 
diff --git a/theory/forget_algebra.v b/theory/forget_algebra.v
index ef12dd1..87a64f9 100644
--- a/theory/forget_algebra.v
+++ b/theory/forget_algebra.v
@@ -2,9 +2,9 @@
 
 This functor should nicely compose with the one forgetting variety laws. *)
 Require Import
-  abstract_algebra universal_algebra interfaces.functors
-  ua_homomorphisms theory.categories
-  categories.setoids categories.product categories.algebras.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors
+  MathClasses.theory.ua_homomorphisms MathClasses.theory.categories
+  MathClasses.categories.setoids MathClasses.categories.product MathClasses.categories.algebras.
 
 Section contents.
   Variable sign: Signature.
diff --git a/theory/forget_variety.v b/theory/forget_variety.v
index c48cdb6..638b86a 100644
--- a/theory/forget_variety.v
+++ b/theory/forget_variety.v
@@ -1,8 +1,8 @@
 (* "Forgetting" a variety's laws (but keeping the algebraic operations) is a trivial functor. *)
 
 Require Import
-  canonical_names universal_algebra interfaces.functors
-  theory.categories categories.varieties categories.algebras.
+  MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors
+  MathClasses.theory.categories MathClasses.categories.varieties MathClasses.categories.algebras.
 
 Section contents.
 
diff --git a/theory/functors.v b/theory/functors.v
index 86839b2..f762525 100644
--- a/theory/functors.v
+++ b/theory/functors.v
@@ -1,8 +1,8 @@
 Require Import
-  canonical_names abstract_algebra
-  interfaces.functors.
+  MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra
+  MathClasses.interfaces.functors.
 Require
-  categories.setoids.
+  MathClasses.categories.setoids.
 
 Section setoid_functor_as_posh_functor.
 Context `{Pfunctor : @SFunctor F map_eq map}.
diff --git a/theory/groups.v b/theory/groups.v
index 091424d..725d5a0 100644
--- a/theory/groups.v
+++ b/theory/groups.v
@@ -1,7 +1,7 @@
 Require
-  theory.setoids.
+  MathClasses.theory.setoids.
 Require Import
-  Morphisms abstract_algebra.
+  Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra.
 
 Section semigroup_props.
 Context `{SemiGroup G}.
diff --git a/theory/hom_functor.v b/theory/hom_functor.v
index 02ab018..33fc110 100644
--- a/theory/hom_functor.v
+++ b/theory/hom_functor.v
@@ -1,6 +1,6 @@
 Require Import
-  abstract_algebra theory.setoids interfaces.functors theory.categories.
-Require categories.setoids.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories.
+Require MathClasses.categories.setoids.
 
 Section contents.
   Context `{Category C} (x: C).
diff --git a/theory/int_abs.v b/theory/int_abs.v
index d1fa00f..ea6c595 100644
--- a/theory/int_abs.v
+++ b/theory/int_abs.v
@@ -1,6 +1,6 @@
 Require Import
-  Ring interfaces.naturals abstract_algebra interfaces.orders
-  orders.nat_int theory.integers theory.rings orders.rings.
+  Coq.setoid_ring.Ring 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.
 Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt} `{Naturals N}.
diff --git a/theory/int_pow.v b/theory/int_pow.v
index f5c7b82..a045d53 100644
--- a/theory/int_pow.v
+++ b/theory/int_pow.v
@@ -1,10 +1,10 @@
 Require
-  theory.naturals orders.semirings orders.integers orders.dec_fields.
+  MathClasses.theory.naturals MathClasses.orders.semirings MathClasses.orders.integers MathClasses.orders.dec_fields.
 Require Import
-  Ring Field
-  abstract_algebra interfaces.naturals interfaces.integers
-  interfaces.additional_operations interfaces.orders
-  theory.nat_pow theory.int_abs theory.dec_fields.
+  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.
 
 (* * Properties of Int Pow *)
 Section int_pow_properties.
diff --git a/theory/int_to_nat.v b/theory/int_to_nat.v
index 50f538f..e4251f9 100644
--- a/theory/int_to_nat.v
+++ b/theory/int_to_nat.v
@@ -1,6 +1,6 @@
 Require Import
-  Ring interfaces.naturals abstract_algebra interfaces.orders
-  orders.nat_int theory.integers theory.rings orders.rings.
+  Coq.setoid_ring.Ring 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. 
 Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt} `{Naturals N}.
diff --git a/theory/integers.v b/theory/integers.v
index a4d216e..e0d0bee 100644
--- a/theory/integers.v
+++ b/theory/integers.v
@@ -1,10 +1,10 @@
 (* General results about arbitrary integer implementations. *)
 Require
- theory.nat_distance.
+ MathClasses.theory.nat_distance.
 Require Import
- Ring interfaces.naturals abstract_algebra natpair_integers.
+ Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers.
 Require Export
- interfaces.integers.
+ MathClasses.interfaces.integers.
 
 (* Any two integer implementations are trivially isomorphic because of their initiality,
  but it's nice to have this stated in terms of integers_to_ring being self-inverse: *)
diff --git a/theory/jections.v b/theory/jections.v
index 4f6f045..69a1b3c 100644
--- a/theory/jections.v
+++ b/theory/jections.v
@@ -1,5 +1,5 @@
 Require Import
-  theory.setoids abstract_algebra.
+  MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra.
 
 Local Existing Instance injective_mor.
 Local Existing Instance surjective_mor.
diff --git a/theory/lattices.v b/theory/lattices.v
index 005ba76..109ace8 100644
--- a/theory/lattices.v
+++ b/theory/lattices.v
@@ -1,7 +1,7 @@
 Require Import
-  abstract_algebra theory.groups.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.groups.
 Require
-  varieties.semigroups varieties.monoids.
+  MathClasses.varieties.semigroups MathClasses.varieties.monoids.
 
 Instance bounded_sl_is_sl `{BoundedSemiLattice L} : SemiLattice L.
 Proof. repeat (split; try apply _). Qed.
diff --git a/theory/monads.v b/theory/monads.v
index c221440..677ee1c 100644
--- a/theory/monads.v
+++ b/theory/monads.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra interfaces.monads theory.functors.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors.
 
 Instance default_mon_join `{MonadBind M} : MonadJoin M | 20 := λ _, bind id.
 Instance default_mon_map `{MonadReturn M} `{MonadBind M} : SFmap M | 20 := λ _ _ f, bind (ret ∘ f).
diff --git a/theory/monoid_normalization.v b/theory/monoid_normalization.v
index a5881cc..06b42db 100644
--- a/theory/monoid_normalization.v
+++ b/theory/monoid_normalization.v
@@ -1,6 +1,6 @@
-Require Import Omega.
-Require Import abstract_algebra ua_packed.
-Require universal_algebra varieties.monoids.
+Require Import Coq.omega.Omega.
+Require Import MathClasses.interfaces.abstract_algebra MathClasses.theory.ua_packed.
+Require MathClasses.interfaces.universal_algebra MathClasses.varieties.monoids.
 
 Notation msig := varieties.monoids.sig.
 Notation Op := (universal_algebra.Op msig False).
diff --git a/theory/nat_distance.v b/theory/nat_distance.v
index 71b4e02..120f16c 100644
--- a/theory/nat_distance.v
+++ b/theory/nat_distance.v
@@ -1,7 +1,7 @@
 Require
-  orders.naturals peano_naturals.
+  MathClasses.orders.naturals MathClasses.implementations.peano_naturals.
 Require Import
-  Ring abstract_algebra interfaces.naturals interfaces.orders interfaces.additional_operations.
+  Coq.setoid_ring.Ring 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 1f75b27..ff4deac 100644
--- a/theory/nat_pow.v
+++ b/theory/nat_pow.v
@@ -1,7 +1,7 @@
 Require
-  theory.naturals.
+  MathClasses.theory.naturals.
 Require Import
-  Ring abstract_algebra interfaces.naturals interfaces.orders interfaces.additional_operations.
+  Coq.setoid_ring.Ring 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 edc3d56..0358ab5 100644
--- a/theory/naturals.v
+++ b/theory/naturals.v
@@ -1,8 +1,8 @@
 Require Import
-  Ring abstract_algebra peano_naturals theory.rings
-  categories.varieties theory.ua_transference.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings
+  MathClasses.categories.varieties MathClasses.theory.ua_transference.
 Require Export
-  interfaces.naturals.
+  MathClasses.interfaces.naturals.
 
 Lemma to_semiring_involutive N `{Naturals N} N2 `{Naturals N2} x :
   naturals_to_semiring N2 N (naturals_to_semiring N N2 x) = x.
diff --git a/theory/products.v b/theory/products.v
index f14dd14..16869c8 100644
--- a/theory/products.v
+++ b/theory/products.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra.
+  MathClasses.interfaces.abstract_algebra.
 
 Definition prod_equiv `{Equiv A} `{Equiv B} : Equiv (A * B) := λ p q, fst p = fst q ∧ snd p = snd q.
 (* Avoid eager application *)
diff --git a/theory/quote_monoid.v b/theory/quote_monoid.v
index c813718..8bae0eb 100644
--- a/theory/quote_monoid.v
+++ b/theory/quote_monoid.v
@@ -1,10 +1,10 @@
-Require Import abstract_algebra.
-Require universal_algebra.
+Require Import MathClasses.interfaces.abstract_algebra.
+Require MathClasses.interfaces.universal_algebra.
 
 Module ua := universal_algebra.
 
-Require varieties.monoids.
-Require monoid_normalization.
+Require MathClasses.varieties.monoids.
+Require MathClasses.theory.monoid_normalization.
 
 Notation msig := varieties.monoids.sig.
 Notation Op := (ua.Op msig False).
diff --git a/theory/rationals.v b/theory/rationals.v
index 9e865f4..30bdf6d 100644
--- a/theory/rationals.v
+++ b/theory/rationals.v
@@ -1,8 +1,8 @@
 Require Import
-  Ring
-  abstract_algebra interfaces.integers interfaces.naturals interfaces.rationals
-  field_of_fractions natpair_integers
-  theory.rings theory.integers theory.dec_fields.
+  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.
 
 Program Instance slow_rat_dec `{Rationals Q} : ∀ x y: Q, Decision (x = y) | 10 := λ x y,
   match decide (rationals_to_frac Q (SRpair nat) x = rationals_to_frac Q (SRpair nat) y) with
diff --git a/theory/ring_congruence.v b/theory/ring_congruence.v
index bf39995..d3a5f01 100644
--- a/theory/ring_congruence.v
+++ b/theory/ring_congruence.v
@@ -1,5 +1,5 @@
 Require Import
-  Ring abstract_algebra theory.rings.
+  Coq.setoid_ring.Ring 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 aa8b710..2938f67 100644
--- a/theory/ring_ideals.v
+++ b/theory/ring_ideals.v
@@ -1,9 +1,9 @@
  (* We define what a ring ideal is, show that they yield congruences,
  define what a kernel is, and show that kernels are ideal. *)
 Require Import
-  Ring abstract_algebra theory.rings.
+  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings.
 Require Export
-   theory.ring_congruence.
+   MathClasses.theory.ring_congruence.
 
 (* Require ua_congruence varieties.rings. *)
 
diff --git a/theory/rings.v b/theory/rings.v
index b3b49a3..42282f1 100644
--- a/theory/rings.v
+++ b/theory/rings.v
@@ -1,7 +1,7 @@
 Require
-  varieties.monoids theory.groups strong_setoids.
+  MathClasses.varieties.monoids MathClasses.theory.groups MathClasses.theory.strong_setoids.
 Require Import
-  Ring abstract_algebra.
+  Coq.setoid_ring.Ring 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/sequences.v b/theory/sequences.v
index 5779ba0..2b28843 100644
--- a/theory/sequences.v
+++ b/theory/sequences.v
@@ -1,8 +1,8 @@
 Require Import
-  theory.categories
-  interfaces.functors
-  abstract_algebra
-  interfaces.sequences.
+  MathClasses.theory.categories
+  MathClasses.interfaces.functors
+  MathClasses.interfaces.abstract_algebra
+  MathClasses.interfaces.sequences.
 
 Section contents.
   Context `{Sequence sq}.
diff --git a/theory/series.v b/theory/series.v
index 57fd458..0dc2efb 100644
--- a/theory/series.v
+++ b/theory/series.v
@@ -1,8 +1,8 @@
 Require Import
-  Ring Factorial workaround_tactics
-  abstract_algebra interfaces.additional_operations interfaces.orders
-  interfaces.naturals interfaces.integers
-  theory.nat_pow theory.int_pow theory.streams.
+  Coq.setoid_ring.Ring Coq.Arith.Factorial 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.
 
 Local Existing Instance srorder_semiring.
 
diff --git a/theory/setoids.v b/theory/setoids.v
index c1d7dc4..fcf156e 100644
--- a/theory/setoids.v
+++ b/theory/setoids.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra theory.products.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.products.
 
 Lemma ext_equiv_refl `{Setoid_Morphism A B f} : f = f.
 Proof. intros ?? E. pose proof (setoidmor_b f). now rewrite E. Qed.
diff --git a/theory/shiftl.v b/theory/shiftl.v
index 5902725..0e60bce 100644
--- a/theory/shiftl.v
+++ b/theory/shiftl.v
@@ -1,9 +1,9 @@
 Require
-  orders.integers theory.dec_fields theory.nat_pow.
+  MathClasses.orders.integers MathClasses.theory.dec_fields MathClasses.theory.nat_pow.
 Require Import
-  Ring
-  abstract_algebra interfaces.naturals interfaces.integers
-  interfaces.additional_operations interfaces.orders.
+  Coq.setoid_ring.Ring
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers
+  MathClasses.interfaces.additional_operations MathClasses.interfaces.orders.
 
 Section shiftl.
 Context `{SemiRing A} `{!LeftCancellation (.*.) (2:A)} `{SemiRing B} `{!Biinduction B} `{!ShiftLSpec A B sl}.
diff --git a/theory/streams.v b/theory/streams.v
index 8397103..4f6bf41 100644
--- a/theory/streams.v
+++ b/theory/streams.v
@@ -1,7 +1,7 @@
 (* In the standard library equality on streams is defined as pointwise Leibniz equality.
     Here we prove similar results, but we use setoid equality instead. *)
-Require Export Streams.
-Require Import peano_naturals abstract_algebra.
+Require Export Coq.Lists.Streams.
+Require Import MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra.
 
 Section streams.
 Context `{Setoid A}.
diff --git a/theory/strong_setoids.v b/theory/strong_setoids.v
index 9a2bc17..6373752 100644
--- a/theory/strong_setoids.v
+++ b/theory/strong_setoids.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra jections.
+  MathClasses.interfaces.abstract_algebra MathClasses.theory.jections.
 
 Section contents.
 Context `{StrongSetoid A}.
diff --git a/theory/ua_congruence.v b/theory/ua_congruence.v
index b9927ad..ecbf24f 100644
--- a/theory/ua_congruence.v
+++ b/theory/ua_congruence.v
@@ -1,9 +1,9 @@
 Require Import
-  Morphisms RelationClasses Relation_Definitions List
-  universal_algebra ua_homomorphisms canonical_names ua_subalgebraT util.
-Require ua_products.
+  Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List
+  MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util.
+Require MathClasses.theory.ua_products.
 
-Require theory.categories.
+Require MathClasses.theory.categories.
 
 (* Remove this *)
 Local Hint Transparent Equiv : typeclass_instances.
diff --git a/theory/ua_homomorphisms.v b/theory/ua_homomorphisms.v
index 709a0b4..2f45671 100644
--- a/theory/ua_homomorphisms.v
+++ b/theory/ua_homomorphisms.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra universal_algebra.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra.
 
 Section contents.
   Variable σ: Signature.
diff --git a/theory/ua_mapped_operations.v b/theory/ua_mapped_operations.v
index d40cd50..33783d5 100644
--- a/theory/ua_mapped_operations.v
+++ b/theory/ua_mapped_operations.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra universal_algebra.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra.
 
 Section contents.
   Variable Sorts: Set.
diff --git a/theory/ua_packed.v b/theory/ua_packed.v
index cecb08f..4f6fd5a 100644
--- a/theory/ua_packed.v
+++ b/theory/ua_packed.v
@@ -1,5 +1,5 @@
 Require Import
-  canonical_names universal_algebra Program.
+  MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra Coq.Program.Program.
 
 Section packed.
   Context (σ: Signature) {V: Type}.
diff --git a/theory/ua_products.v b/theory/ua_products.v
index f21e356..2880fb3 100644
--- a/theory/ua_products.v
+++ b/theory/ua_products.v
@@ -1,8 +1,8 @@
 Require Import
-  abstract_algebra
-  universal_algebra ua_homomorphisms
-  theory.categories categories.varieties.
-Require theory.setoids.
+  MathClasses.interfaces.abstract_algebra
+  MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms
+  MathClasses.theory.categories MathClasses.categories.varieties.
+Require MathClasses.theory.setoids.
 
 Section algebras.
   Context
@@ -174,7 +174,7 @@ Section varieties.
   Qed.
 End varieties.
 
-Require categories.varieties.
+Require MathClasses.categories.varieties.
 
 Section categorical.
   Context
diff --git a/theory/ua_subalgebra.v b/theory/ua_subalgebra.v
index 85684c9..1d24cad 100644
--- a/theory/ua_subalgebra.v
+++ b/theory/ua_subalgebra.v
@@ -1,8 +1,8 @@
 Require Import
-  RelationClasses
-  universal_algebra ua_homomorphisms canonical_names theory.categories abstract_algebra.
+  Coq.Classes.RelationClasses
+  MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.interfaces.abstract_algebra.
 Require
-  categories.algebras forget_algebra.
+  MathClasses.categories.algebras MathClasses.theory.forget_algebra.
 
 Section subalgebras.
   Context `{Algebra sign A} (P: ∀ s, A s → Prop).
diff --git a/theory/ua_subalgebraT.v b/theory/ua_subalgebraT.v
index 3a107c5..b1a824e 100644
--- a/theory/ua_subalgebraT.v
+++ b/theory/ua_subalgebraT.v
@@ -4,10 +4,10 @@ instead of Prop (and with carrier sigT instead of sig).
 Hopefully one day Coq's universe polymorphism will permit a merge of sig and sigT,
 at which point we may try to merge ua_subalgebra and ua_subalgebraT as well. *)
 Require Import
-  RelationClasses
-  universal_algebra ua_homomorphisms theory.categories abstract_algebra.
+  Coq.Classes.RelationClasses
+  MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories MathClasses.interfaces.abstract_algebra.
 Require
-  categories.algebras.
+  MathClasses.categories.algebras.
 
 Section subalgebras.
   Context `{Algebra sign A} (P: ∀ s, A s → Type).
diff --git a/theory/ua_subvariety.v b/theory/ua_subvariety.v
index bacb143..a86da26 100644
--- a/theory/ua_subvariety.v
+++ b/theory/ua_subvariety.v
@@ -1,6 +1,6 @@
 Require Import
-  RelationClasses Morphisms Program
-  universal_algebra canonical_names ua_subalgebra.
+  Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Program.Program
+  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
 they yield subalgebras. We now expand on this result and show that they
diff --git a/theory/ua_term_monad.v b/theory/ua_term_monad.v
index 98e6cf9..9c5360b 100644
--- a/theory/ua_term_monad.v
+++ b/theory/ua_term_monad.v
@@ -1,5 +1,5 @@
 Require Import
-  abstract_algebra universal_algebra interfaces.monads.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.monads.
 
 Section contents.
   Context (operation: Set) (operation_type: operation → OpType unit).
diff --git a/theory/ua_transference.v b/theory/ua_transference.v
index 2b20098..25f51a8 100644
--- a/theory/ua_transference.v
+++ b/theory/ua_transference.v
@@ -1,8 +1,8 @@
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms
-  canonical_names theory.categories ua_mapped_operations.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms
+  MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.theory.ua_mapped_operations.
 
-Require categories.varieties.
+Require MathClasses.categories.varieties.
 
 Section contents.
 
diff --git a/varieties/abgroup.v b/varieties/abgroup.v
index 91933cf..0736dfe 100644
--- a/varieties/abgroup.v
+++ b/varieties/abgroup.v
@@ -1,8 +1,8 @@
 (* To be imported qualified. *)
 Require
-  categories.varieties categories.product forget_algebra forget_variety theory.groups.
+  MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety MathClasses.theory.groups.
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms workaround_tactics.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics.
 
 Inductive op := mult | inv | one.
 
diff --git a/varieties/closed_terms.v b/varieties/closed_terms.v
index f5a5d2f..f331931 100644
--- a/varieties/closed_terms.v
+++ b/varieties/closed_terms.v
@@ -1,8 +1,8 @@
 Require Import
-  RelationClasses Relation_Definitions List Morphisms
-  universal_algebra ua_homomorphisms
-  abstract_algebra canonical_names
-  theory.categories categories.varieties.
+  Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Classes.Morphisms
+  MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names
+  MathClasses.theory.categories MathClasses.categories.varieties.
 
 Section contents.
   Variable et: EquationalTheory.
diff --git a/varieties/empty.v b/varieties/empty.v
index 2b15791..d6681c6 100644
--- a/varieties/empty.v
+++ b/varieties/empty.v
@@ -1,7 +1,7 @@
 Require
-  theory.rings categories.varieties.
+  MathClasses.theory.rings MathClasses.categories.varieties.
 Require Import
-  abstract_algebra universal_algebra.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra.
 
 Definition op := False.
 
diff --git a/varieties/groups.v b/varieties/groups.v
index 6e7c69b..43b722c 100644
--- a/varieties/groups.v
+++ b/varieties/groups.v
@@ -1,8 +1,8 @@
 (* To be imported qualified. *)
 Require
-  categories.varieties categories.product forget_algebra forget_variety theory.groups.
+  MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety MathClasses.theory.groups.
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms workaround_tactics.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics.
 
 Inductive op := mult | inv | one.
 
diff --git a/varieties/monoids.v b/varieties/monoids.v
index f1c736c..78c07da 100644
--- a/varieties/monoids.v
+++ b/varieties/monoids.v
@@ -1,9 +1,9 @@
 (* To be imported qualified. *)
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms workaround_tactics
-  categories.categories.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics
+  MathClasses.categories.categories.
 Require
-  categories.varieties categories.product forget_algebra forget_variety.
+  MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety.
 
 Inductive op := mult | one.
 
diff --git a/varieties/open_terms.v b/varieties/open_terms.v
index 526042d..0d1f5d8 100644
--- a/varieties/open_terms.v
+++ b/varieties/open_terms.v
@@ -1,7 +1,7 @@
 Require Import
-  RelationClasses Relation_Definitions List Morphisms
-  universal_algebra abstract_algebra canonical_names
-  theory.categories categories.varieties.
+  Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Classes.Morphisms
+  MathClasses.interfaces.universal_algebra MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names
+  MathClasses.theory.categories MathClasses.categories.varieties.
 
 Section contents.
   Context
diff --git a/varieties/rings.v b/varieties/rings.v
index 1cbcc57..c4c1024 100644
--- a/varieties/rings.v
+++ b/varieties/rings.v
@@ -1,9 +1,9 @@
 (* To be imported qualified. *)
 Require
-  categories.varieties theory.rings.
+  MathClasses.categories.varieties MathClasses.theory.rings.
 Require Import
-  Ring
-  abstract_algebra universal_algebra ua_homomorphisms workaround_tactics.
+  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.
 
diff --git a/varieties/semigroups.v b/varieties/semigroups.v
index d4dd808..7d522ce 100644
--- a/varieties/semigroups.v
+++ b/varieties/semigroups.v
@@ -1,8 +1,8 @@
 (* To be imported qualified. *)
 Require
-  categories.varieties categories.product forget_algebra forget_variety.
+  MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety.
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms workaround_tactics.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics.
 
 Inductive op := mult.
 
diff --git a/varieties/semirings.v b/varieties/semirings.v
index 4fc8910..ea977d6 100644
--- a/varieties/semirings.v
+++ b/varieties/semirings.v
@@ -1,8 +1,8 @@
 (* To be imported qualified. *)
 Require
-  theory.rings categories.varieties.
+  MathClasses.theory.rings MathClasses.categories.varieties.
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms workaround_tactics.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics.
 
 Inductive op := plus | mult | zero | one.
 
diff --git a/varieties/setoids.v b/varieties/setoids.v
index fee4ec4..1564030 100644
--- a/varieties/setoids.v
+++ b/varieties/setoids.v
@@ -1,7 +1,7 @@
 Require
-  categories.varieties.
+  MathClasses.categories.varieties.
 Require Import
-  abstract_algebra universal_algebra ua_homomorphisms.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms.
 
 Definition op := False.