Adapt to coq/coq#19530

src/Algebra/IntegralDomain.v

@@ -173,7 +173,7 @@ End IntegralDomain.
 
 (** Tactics for polynomial equations over integral domains *)
 
-Require Coq.nsatz.Nsatz.
+From Coq Require NsatzTactic.
 
 Ltac dropAlgebraSyntax :=
   cbv beta delta [

src/Algebra/Nsatz.v

@@ -2,28 +2,17 @@
   periodically check whether we still need it -- once enough bugs get fixed
   in mailine, we hope to drop this implementation *)
 
-Require Coq.nsatz.Nsatz.
-Require Import Coq.Lists.List.
+From Coq Require NsatzTactic.
+From Coq Require Import List.
 Require Export Crypto.Util.FixCoqMistakes.
 
-(** For compat with https://github.com/coq/coq/pull/12073 *)
-Module Nsatz.
-  Import nsatz.Nsatz.
-  Notation check_correct := check_correct.
-  Ltac Nsatz_nsatz := nsatz.
-  Ltac nsatz := Nsatz_nsatz.
-  Notation PEevalR := PEevalR.
-  Notation psos_r1 := psos_r1.
-  Notation psos_r1b := psos_r1b.
-End Nsatz.
-
 Generalizable All Variables.
 Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)}
   : forall x y, eq (sub x y) zero <-> eq x y.
 Proof.
   split;intros Hx.
-  { eapply Nsatz.psos_r1b. eapply Hx. }
-  { eapply Nsatz.psos_r1. eapply Hx. }
+  { eapply NsatzTactic.psos_r1b. eapply Hx. }
+  { eapply NsatzTactic.psos_r1. eapply Hx. }
 Qed.
 
 Ltac get_goal := lazymatch goal with |- ?g => g end.
@@ -54,15 +43,9 @@ Ltac nsatz_get_reified_goal reified_package :=
   lazymatch reified_package with (_, _, ?goal) => goal end.
 
 Require Import Coq.setoid_ring.Ring_polynom.
-(* Kludge for 8.4/8.5 compatibility *)
-Module Import mynsatz_compute.
-  Import nsatz.Nsatz.
-  Global Ltac mynsatz_compute x := nsatz_compute x.
-End mynsatz_compute.
-Ltac nsatz_compute x := mynsatz_compute x.
 
 Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens :=
-  nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens).
+  NsatzTactic.nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens).
 
 Ltac nsatz_compute_get_leading_coefficient :=
   lazymatch goal with
@@ -111,15 +94,15 @@ Ltac nsatz_domain_sugar_power domain sugar power :=
     nsatz_rewrite_and_revert domain;
     let reified_package := nsatz_reify_equations eq zero in
     let fv := nsatz_get_free_variables reified_package in
-    let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in
+    let interp := constr:(@NsatzTactic.PEevalR _ _ _ _ _ _ _ _ Fops fv) in
     let reified_givens := nsatz_get_reified_givens reified_package in
     let reified_goal := nsatz_get_reified_goal reified_package in
     nsatz_compute_to_goal sugar nparams reified_goal power reified_givens;
     let a := nsatz_compute_get_leading_coefficient in
     let crt := nsatz_compute_get_certificate in
     intros _ (* discard [nsatz_compute] output *); intros;
-    apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
-    [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
+    apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@NsatzTactic.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
+    [ nsatz_nonzero; cbv iota beta delta [NsatzTactic.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
     | solve [vm_cast_no_check (eq_refl true)] (* if this fails, the prover returned a bad certificate *)
     | solve [repeat (split; [assumption|]); exact I] ]
   end.
@@ -182,7 +165,7 @@ Module Export Hints.
          Ncring_initial.gen_phiZ_morph
          Ncring_initial.multiplication_phi_ring
   .
-  Import nsatz.Nsatz.
+  Import NsatzTactic.
   Global Existing Instances
          Qops
          Qri

src/Arithmetic/ModularArithmeticTheorems.v

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

src/Arithmetic/PrimeFieldTheorems.v

@@ -2,7 +2,7 @@ Require Export Crypto.Spec.ModularArithmetic.
 Require Export Crypto.Arithmetic.ModularArithmeticTheorems.
 Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac.
 
-Require Import Coq.nsatz.Nsatz.
+From Coq Require Import NsatzTactic.
 Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Crypto.Arithmetic.ModularArithmeticPre.
 Require Import Crypto.Util.NumTheoryUtil.

src/Compilers/MapBaseType.v

@@ -1,4 +1,4 @@
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.ExprInversion.

src/Compilers/MapBaseTypeWf.v

@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Wf.

src/Compilers/Named/AListContext.v

@@ -1,6 +1,6 @@
 (** * Context made from an associative list, without modules *)
-Require Import Coq.Bool.Sumbool.
-Require Import Coq.Lists.List.
+From Coq Require Import Sumbool.
+From Coq Require Import List.
 Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Util.Tactics.BreakMatch.

src/Compilers/Named/FMapContext.v

@@ -1,4 +1,4 @@
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 Require Import Coq.FSets.FMapInterface.
 Require Import Coq.FSets.FMapFacts.
 Require Import Crypto.Compilers.Named.Context.

src/Compilers/Named/MapCast.v

@@ -1,4 +1,4 @@
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Named.Context.

src/Compilers/Named/MapCastInterp.v

@@ -1,5 +1,5 @@
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Relations.

src/Compilers/Named/MapCastWf.v

@@ -1,5 +1,5 @@
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Relations.

src/Compilers/Named/MapType.v

@@ -1,4 +1,4 @@
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Named.Syntax.

src/Primitives/MxDHRepChange.v

@@ -1,4 +1,4 @@
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import SetoidList.
 Require Import Crypto.Spec.MxDH.
 Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.Ring Crypto.Algebra.Field.
 Require Import Crypto.Util.Tuple Crypto.Util.Prod.

src/Util/AdditionChainExponentiation.v

@@ -1,5 +1,5 @@
 Require Import Coq.funind.FunInd.
-Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations.
+From Coq Require Import List SetoidList. Import ListNotations.
 Require Import Coq.Numbers.BinNums Coq.NArith.BinNat.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.

src/Util/Factorize.v

@@ -1,4 +1,4 @@
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 Require Import Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.NArith.NArith.
 Require Import Coq.PArith.PArith.

src/Util/ListUtil.v

@@ -1819,7 +1819,7 @@ Hint Rewrite <- @firstn_update_nth : pull_firstn.
 #[global]
 Hint Rewrite <- @firstn_update_nth : push_update_nth.
 
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import SetoidList.
 Global Instance Proper_nth_default : forall A eq,
   Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)).
 Proof.

src/Util/ListUtil/SetoidList.v

@@ -1,6 +1,6 @@
 Require Import Coq.Lists.List.
 Require Import Coq.Setoids.Setoid.
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import SetoidList.
 Require Import Crypto.Util.Option.
 
 Import ListNotations.

src/Util/MSetPositive/Facts.v

@@ -1,7 +1,7 @@
 Require Import Coq.Setoids.Setoid.
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.Lists.List.
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import SetoidList.
 Require Import Coq.MSets.MSetPositive.
 Require Import Coq.MSets.MSetFacts.
 Require Import Crypto.Util.Tactics.BreakMatch.

src/Util/Tuple.v

@@ -1156,7 +1156,7 @@ Proof.
     repeat intro; subst; auto; reflexivity.
 Qed.
 
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import SetoidList.
 
 Global Instance fieldwise'_Proper
   : forall {n A B}, Proper (pointwise_relation _ (pointwise_relation _ impl) ==> eq ==> eq ==> impl) (@fieldwise' A B n) | 10.