Adapt to https://github.com/coq/coq/pull/19530

LiveVerif/src/LiveVerif/LiveFwd.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
+From Coq Require Import ZArith. Local Open Scope Z_scope.
 Require Import coqutil.Word.Bitwidth.
 Require Import coqutil.Tactics.autoforward.
 Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Map.Interface.

LiveVerif/src/LiveVerif/LiveParsing.v

@@ -1,6 +1,6 @@
-Require Import Coq.setoid_ring.InitialRing. (* for isZcst *)
-Require Import Coq.Strings.String.
-Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
+From Coq Require Import InitialRing. (* for isZcst *)
+From Coq Require Import String.
+From Coq Require Import ZArith. Local Open Scope Z_scope.
 Require Import bedrock2.Syntax.
 Require Import LiveVerif.LiveExpr.
 Require Import LiveVerif.LiveSnippet.

LiveVerif/src/LiveVerif/LiveProgramLogic.v

@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
-Require Import Coq.micromega.Lia.
+From Coq Require Import ZArith. Local Open Scope Z_scope.
+From Coq Require Import Lia.
 Require Import coqutil.Z.Lia.
-Require Import Coq.Strings.String.
+From Coq Require Import String.
 Require Import coqutil.Tactics.rdelta.
 Require Import coqutil.Tactics.Tactics.
 Require Import coqutil.Map.Interface coqutil.Map.Properties.

LiveVerif/src/LiveVerif/LiveRules.v

@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Init.Byte.
-Require Import Coq.Strings.String.
+From Coq Require Import ZArith. Local Open Scope Z_scope.
+From Coq Require Import Lia.
+From Coq.Init Require Import Byte.
+From Coq Require Import String.
 Require Import coqutil.Map.Interface coqutil.Map.Properties.
 Require coqutil.Map.SortedListString. (* for function env, other maps are kept abstract *)
 Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth.

LiveVerif/src/LiveVerif/LiveSnippet.v

@@ -1,4 +1,4 @@
-Require Import Coq.Strings.String.
+From Coq Require Import String.
 Require Import bedrock2.Syntax.
 
 Inductive assignment_rhs :=

LiveVerif/src/LiveVerif/LiveVerifLib.v

@@ -1,5 +1,5 @@
-Require Export Coq.ZArith.ZArith. Local Open Scope Z_scope.
-Require Export Coq.micromega.Lia.
+Require Export ZArith. Local Open Scope Z_scope.
+Require Export Lia.
 Require Export coqutil.Datatypes.Inhabited.
 Require Export coqutil.Tactics.Tactics.
 Require Export coqutil.Tactics.safe_auto.

LiveVerif/src/LiveVerif/PackageContext.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
+From Coq Require Import ZArith. Local Open Scope Z_scope.
 Require Import Ltac2.Ltac2. Set Default Proof Mode "Classic".
 Require Import coqutil.Tactics.rdelta.
 Require Import coqutil.Datatypes.Inhabited.

LiveVerif/src/LiveVerif/string_to_ident.v

@@ -1,5 +1,5 @@
-Require Import Coq.Strings.String.
-Require Import Coq.Strings.Ascii.
+From Coq Require Import String.
+From Coq Require Import Ascii.
 Require Import Ltac2.Ltac2.
 Require Ltac2.Option.
 

LiveVerif/src/LiveVerifExamples/Tests/PrintSmt.v

@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import coqutil.Word.Interface.
-Require Import Coq.Logic.Classical_Prop.
+From Coq Require Import Classical_Prop.
 Require Import coqutil.Tactics.ident_ops.
 
 Ltac eval_constant_pows :=

LiveVerif/src/LiveVerifExamples/Tests/SampleSideconds.v

@@ -26,7 +26,7 @@ Ltac eval_constant_pows :=
              end
          end.
 
-Require Import Coq.Logic.Classical_Prop.
+From Coq Require Import Classical_Prop.
 
 Lemma ExistsNot_NotForall: forall AA (P: AA -> Prop), (exists a: AA, ~ P a) <-> ~ forall (a: AA), P a.
 Proof.

LiveVerif/src/LiveVerifExamples/Tests/SampleSimpls.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
+From Coq Require Import ZArith. Local Open Scope Z_scope.
 Require Import coqutil.Word.Interface coqutil.Word.Properties.
 Require Import coqutil.Datatypes.ZList.
 Require bedrock2.WordNotations.

LiveVerif/src/LiveVerifExamples/interleave.v

@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+From Coq Require Import List.
 Require Import bedrock2.ReversedListNotations. Local Open Scope list_scope.
 
 Section Interleave.