Adapt to coq/coq#19530 (#1957)

src/AbstractInterpretation/AbstractInterpretation.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.

src/AbstractInterpretation/Proofs.v

@@ -1,8 +1,8 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Classes.RelationPairs.
-Require Import Coq.Relations.Relations.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Morphisms.
+From Coq Require Import RelationPairs.
+From Coq Require Import Relations.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.ZRange.BasicLemmas.

src/AbstractInterpretation/Wf.v

@@ -1,8 +1,8 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Classes.RelationPairs.
-Require Import Coq.Relations.Relations.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Morphisms.
+From Coq Require Import RelationPairs.
+From Coq Require Import Relations.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.Sum.
 Require Import Crypto.Util.LetIn.

src/AbstractInterpretation/ZRange.v

@@ -1,5 +1,5 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
 Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.

src/AbstractInterpretation/ZRangeCommonProofs.v

@@ -1,6 +1,6 @@
 (* Proofs shared by Wf and Proofs *)
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relations.
+From Coq Require Import Morphisms.
+From Coq Require Import Relations.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.ListUtil.

src/AbstractInterpretation/ZRangeProofs.v

@@ -1,9 +1,9 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Classes.RelationPairs.
-Require Import Coq.Relations.Relations.
-Require Import Coq.Lists.List.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Morphisms.
+From Coq Require Import RelationPairs.
+From Coq Require Import Relations.
+From Coq Require Import List.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.ZRange.BasicLemmas.

src/Algebra/Field.v

@@ -1,9 +1,9 @@
 Require Import Crypto.Util.Relations Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.DebugPrint.
-Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
+From Coq Require Import RelationClasses Morphisms.
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain.
-Require Coq.setoid_ring.Field_theory.
+From Coq Require Field_theory.
 
 Section Field.
   Context {T eq zero one opp add mul sub inv div} `{@field T eq zero one opp add sub mul inv div}.

src/Algebra/Field_test.v

@@ -1,4 +1,4 @@
-Require Import Coq.PArith.BinPosDef.
+From Coq Require Import BinPosDef.
 Require Import Crypto.Util.Decidable Crypto.Util.Notations.
 Require Import Crypto.Algebra.Ring Crypto.Algebra.Field.
 

src/Algebra/Group.v

@@ -1,4 +1,5 @@
-Require Import Coq.Classes.Morphisms Crypto.Util.Relations (*Crypto.Util.Tactics*).
+From Coq Require Import Morphisms.
+Require Import Crypto.Util.Relations (*Crypto.Util.Tactics*).
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid.
 
 Section BasicProperties.

src/Algebra/Hierarchy.v

@@ -1,10 +1,10 @@
 Require Export Crypto.Util.FixCoqMistakes.
 Require Export Crypto.Util.Decidable.
 
-Require Coq.PArith.BinPos.
-Require Import Coq.Classes.Morphisms.
+From Coq Require BinPos.
+From Coq Require Import Morphisms.
 
-Require Coq.Lists.List.
+From Coq Require List.
 
 Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
 

src/Algebra/IntegralDomain.v

@@ -1,4 +1,4 @@
-Require Coq.setoid_ring.Integral_domain.
+From Coq Require Integral_domain.
 Require Crypto.Algebra.Nsatz.
 Require Import Crypto.Util.Factorize.
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring.

src/Algebra/Monoid.v

@@ -1,4 +1,4 @@
-Require Import Coq.Classes.Morphisms.
+From Coq Require Import Morphisms.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Algebra.Hierarchy.
 

src/Algebra/Nsatz.v

@@ -2,8 +2,8 @@
   periodically check whether we still need it -- once enough bugs get fixed
   in mailine, we hope to drop this implementation *)
 
-Require Coq.nsatz.NsatzTactic.
-Require Import Coq.Lists.List.
+From Coq Require NsatzTactic.
+From Coq Require Import List.
 
 (** For compat with https://github.com/coq/coq/pull/12073 *)
 Module Nsatz.
@@ -50,7 +50,7 @@ Ltac nsatz_get_reified_givens reified_package :=
 Ltac nsatz_get_reified_goal reified_package :=
   lazymatch reified_package with (_, _, ?goal) => goal end.
 
-Require Import Coq.setoid_ring.Ring_polynom.
+From Coq Require Import Ring_polynom.
 (* Kludge for 8.4/8.5 compatibility *)
 Module Import mynsatz_compute.
   Import Coq.nsatz.NsatzTactic.

src/Algebra/Ring.v

@@ -1,13 +1,13 @@
-Require Coq.setoid_ring.Ncring.
-Require Coq.setoid_ring.Cring.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.micromega.Lia.
+From Coq Require Ncring.
+From Coq Require Cring.
+From Coq Require Import Morphisms.
+From Coq Require Import Lia.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.OnSubterms.
 Require Import Crypto.Util.Tactics.Revert.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group Crypto.Algebra.Monoid.
-Require Coq.ZArith.ZArith Coq.PArith.PArith.
+From Coq Require ZArith PArith.
 
 
 Section Ring.
@@ -451,7 +451,7 @@ Definition char_ge
 Existing Class char_ge.
 
 (*** Tactics for ring equations *)
-Require Export Coq.setoid_ring.Ring_tac.
+From Coq Require Export Ring_tac.
 Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t).
 
 Ltac ring_simplify_subterms_in_all :=

src/Algebra/ScalarMult.v

@@ -1,5 +1,6 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Util.ZUtil.Peano.
-Require Import Coq.Classes.Morphisms.
+From Coq Require Import ZArith Lia.
+Require Import Crypto.Util.ZUtil.Peano.
+From Coq Require Import Morphisms.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group.
 Local Open Scope Z_scope.

src/Algebra/SubsetoidRing.v

@@ -1,14 +1,14 @@
-Require Coq.setoid_ring.Ncring.
-Require Coq.setoid_ring.Cring.
-Require Import Coq.Classes.Morphisms.
+From Coq Require Ncring.
+From Coq Require Cring.
+From Coq Require Import Morphisms.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.OnSubterms.
 Require Import Crypto.Util.Tactics.Revert.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group Crypto.Algebra.Monoid.
 Require Import Crypto.Algebra.Ring.
 Require Import Crypto.Util.Tactics.DestructHead.
-Require Coq.ZArith.ZArith Coq.PArith.PArith.
+From Coq Require ZArith PArith.
 
 
 Section Ring.

src/Arithmetic/BYInv.v

@@ -1,8 +1,8 @@
-Require Import Coq.Bool.Bool.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.nsatz.Nsatz.
-Require Import Coq.micromega.Lia.
+From Coq Require Import Bool.
+From Coq Require Import ZArith.
+From Coq Require Import List.
+From Coq Require Import Nsatz.
+From Coq Require Import Lia.
 Require Import Crypto.Arithmetic.UniformWeight.
 Require Import Crypto.Arithmetic.Saturated.
 Require Import Crypto.Arithmetic.Core.

src/Arithmetic/BarrettReduction.v

@@ -1,6 +1,7 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.derive.Derive.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith Lia.
+Require Import Crypto.Algebra.Nsatz.
+From Coq Require Import Derive.
+From Coq Require Import List.
 Require Import Crypto.Algebra.Ring.
 Require Import Crypto.Arithmetic.BaseConversion.
 Require Import Crypto.Arithmetic.Core.

src/Arithmetic/BarrettReduction/Generalized.v

@@ -8,7 +8,7 @@
     ± 1] to [k ± offset]).  This leads to weaker conditions on the
     base ([b]), exponent ([k]), and the [offset] than those given in
     the HAC. *)
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+From Coq Require Import ZArith Lia.
 Require Import Crypto.Util.ZUtil.Div.
 Require Import Crypto.Util.ZUtil.Modulo.
 Require Import Crypto.Util.ZUtil.Pow.

src/Arithmetic/BarrettReduction/HAC.v

@@ -8,7 +8,7 @@
     does reduction modulo [b^(k+offset)] early (ensuring that we don't
     have to carry around extra precision), but requires more stringint
     conditions on the base ([b]), exponent ([k]), and the [offset]. *)
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+From Coq Require Import ZArith Lia.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.

src/Arithmetic/BarrettReduction/RidiculousFish.v

@@ -1,8 +1,8 @@
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.ZUtil.Hints.ZArith.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
 
 Open Scope Z_scope.
 

src/Arithmetic/BarrettReduction/Wikipedia.v

@@ -1,6 +1,6 @@
 (*** Barrett Reduction *)
 (** This file implements Barrett Reduction on [Z].  We follow Wikipedia. *)
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+From Coq Require Import ZArith Lia.
 Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 Require Import Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.

src/Arithmetic/BaseConversion.v

@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.derive.Derive.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import Derive.
+From Coq Require Import List.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.ModOps.
 Require Import Crypto.Arithmetic.Partition.

src/Arithmetic/BinaryExtendedGCD.v

@@ -1,7 +1,7 @@
-Require Import Coq.Bool.Bool.
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.ZArith.Znumtheory.
+From Coq Require Import Bool.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Znumtheory.
 Require Import Crypto.Util.Loops.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.ZUtil.

src/Arithmetic/Core.v

@@ -1,7 +1,7 @@
 (* Following http://adam.chlipala.net/theses/andreser.pdf chapter 3 *)
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
-Require Import Coq.Structures.Orders.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith Lia.
+From Coq Require Import Orders.
+From Coq Require Import List.
 Require Import Crypto.Algebra.Nsatz.
 Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
 Require Import Crypto.Util.Decidable.

src/Arithmetic/DettmanMultiplication.v

@@ -1,8 +1,8 @@
 Require Import Crypto.Arithmetic.Core.
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith Lia.
+From Coq Require Import List.
 Require Import Crypto.Arithmetic.ModOps.
-Require Import Coq.QArith.QArith_base Coq.QArith.Qround.
+From Coq Require Import QArith_base Qround.
 Local Open Scope list_scope.
 
 Import Associational Positional.

src/Arithmetic/FLia.v

@@ -1,5 +1,5 @@
-Require Import ZArith.ZArith.
-Require Import Coq.micromega.Lia.
+Require Import PArith BinInt ZArith.
+From Coq Require Import Lia.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 
 Local Open Scope Z_scope.

src/Arithmetic/FancyMontgomeryReduction.v

@@ -1,6 +1,7 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.derive.Derive.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith Lia.
+Require Import Crypto.Algebra.Nsatz.
+From Coq Require Import Derive.
+From Coq Require Import List.
 Require Import Crypto.Arithmetic.BaseConversion.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.ModOps.

src/Arithmetic/Freeze.v

@@ -1,5 +1,5 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
+From Coq Require Import ZArith Lia.
+Require Import QArith_base Qround Crypto.Util.QUtil.
 Require Import Crypto.Arithmetic.BaseConversion.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.ModOps.

src/Arithmetic/ModOps.v

@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
-Require Import Coq.derive.Derive.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
+From Coq Require Import ZArith Lia.
+From Coq Require Import Derive.
+Require Import QArith_base Qround Crypto.Util.QUtil.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.

src/Arithmetic/ModularArithmeticPre.v

@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.BinNums Coq.ZArith.Znumtheory.
-Require Import Coq.Logic.Eqdep_dec.
-Require Import Coq.Logic.EqdepFacts.
-Require Import Coq.micromega.Lia.
+From Coq Require Import ZArith NArith BinNums Znumtheory.
+From Coq Require Import Eqdep_dec.
+From Coq Require Import EqdepFacts.
+From Coq Require Import Lia.
 Require Import Crypto.Util.NumTheoryUtil.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Import Crypto.Util.Tactics.BreakMatch.

src/Arithmetic/ModularArithmeticTheorems.v

@@ -1,10 +1,10 @@
-Require Import Coq.micromega.Lia.
+From Coq Require Import Lia.
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.Arithmetic.ModularArithmeticPre.
 
-Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *)
-Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
-Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac.
+From Coq Require Import ZArith Zdiv Znumtheory NArith NArithRing. (* import Zdiv before Znumtheory *)
+From Coq Require Import Morphisms Setoid.
+From Coq Require Export Ring_theory Ring_tac.
 
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult.
 Require Crypto.Algebra.Ring Crypto.Algebra.Field.

src/Arithmetic/MontgomeryReduction/Definition.v

@@ -1,7 +1,7 @@
 (*** Montgomery Multiplication *)
 (** This file implements Montgomery Form, Montgomery Reduction, and
     Montgomery Multiplication on [Z].  We follow Wikipedia. *)
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import Crypto.Util.ZUtil.EquivModulo.
 Require Import Crypto.Util.Notations.
 

src/Arithmetic/MontgomeryReduction/Proofs.v

@@ -2,7 +2,7 @@
 (** This file implements the proofs for Montgomery Form, Montgomery
     Reduction, and Montgomery Multiplication on [Z].  We follow
     Wikipedia. *)
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Coq.Structures.Equalities.
+From Coq Require Import ZArith Lia Equalities.
 Require Import Crypto.Arithmetic.MontgomeryReduction.Definition.
 Require Import Crypto.Util.ZUtil.EquivModulo.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.

src/Arithmetic/Partition.v

@@ -1,7 +1,7 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.Structures.Orders.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
+From Coq Require Import List.
+From Coq Require Import Orders.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.ZUtil.EquivModulo.