Adapt to coq/coq#19530

mit-plv · Sep 17, 2024 · 07ad3e7 · 07ad3e7
1 parent 2223b2a
commit 07ad3e7
Show file tree

Hide file tree

Showing 162 changed files with 1,423 additions and 293 deletions.
diff --git a/LiveVerif/src/LiveVerif/LiveFwd.v b/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.

diff --git a/LiveVerif/src/LiveVerif/LiveParsing.v b/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.

diff --git a/LiveVerif/src/LiveVerif/LiveProgramLogic.v b/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.

diff --git a/LiveVerif/src/LiveVerif/LiveRules.v b/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.

diff --git a/LiveVerif/src/LiveVerif/LiveSnippet.v b/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 :=

diff --git a/LiveVerif/src/LiveVerif/LiveVerifLib.v b/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.

diff --git a/LiveVerif/src/LiveVerif/PackageContext.v b/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.

diff --git a/LiveVerif/src/LiveVerif/string_to_ident.v b/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.
 

diff --git a/LiveVerif/src/LiveVerifExamples/Tests/PrintSmt.v b/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 :=

diff --git a/LiveVerif/src/LiveVerifExamples/Tests/SampleSideconds.v b/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.

diff --git a/LiveVerif/src/LiveVerifExamples/Tests/SampleSimpls.v b/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.

diff --git a/LiveVerif/src/LiveVerifExamples/interleave.v b/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.

diff --git a/LiveVerifEx64/src/LiveVerifExamples/fmalloc.v b/LiveVerifEx64/src/LiveVerifExamples/fmalloc.v