Adapt to coq/coq#19530

mit-plv · Sep 18, 2024 · 3222e19 · 3222e19
1 parent 19f344b
commit 3222e19
Show file tree

Hide file tree

Showing 57 changed files with 220 additions and 220 deletions.
diff --git a/src/Rewriter/Demo.v b/src/Rewriter/Demo.v
@@ -9,7 +9,7 @@ Require Import Rewriter.Util.plugins.RewriterBuild.
 (** We will be working with examples involving arithmetic on [nat] and
     [Z], as well as some examples on [list], so we import the relevant
     files. *)
-Require Import Coq.Arith.Arith Coq.ZArith.ZArith Coq.Lists.List.
+From Coq Require Import Arith ZArith List.
 Import ListNotations. Local Open Scope list_scope.
 
 (** We [Unset Ltac Backtrace] to get prettier error messages. *)

diff --git a/src/Rewriter/Language/IdentifiersBasicGenerate.v b/src/Rewriter/Language/IdentifiersBasicGenerate.v
@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import Bool.
+From Coq Require Import Morphisms.
+From Coq Require Import List.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Bool.
 Require Import Ltac2.Printf.

diff --git a/src/Rewriter/Language/IdentifiersGenerate.v b/src/Rewriter/Language/IdentifiersGenerate.v
@@ -1,8 +1,8 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
-Require Import Coq.derive.Derive.
+From Coq Require Import ZArith.
+From Coq Require Import FMapPositive.
+From Coq Require Import MSetPositive.
+From Coq Require Import List.
+From Coq Require Import Derive.
 Require Import Rewriter.Util.CPSNotations.
 Require Import Rewriter.Util.Option.
 Require Import Rewriter.Util.PrimitiveSigma.

diff --git a/src/Rewriter/Language/IdentifiersGenerateProofs.v b/src/Rewriter/Language/IdentifiersGenerateProofs.v
@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+From Coq Require Import ZArith.
+From Coq Require Import MSetPositive.
+From Coq Require Import FMapPositive.
 Require Import Rewriter.Util.PrimitiveSigma.
 Require Import Rewriter.Util.MSetPositive.Facts.
 Require Import Rewriter.Util.CPSNotations.

diff --git a/src/Rewriter/Language/IdentifiersLibrary.v b/src/Rewriter/Language/IdentifiersLibrary.v
@@ -1,9 +1,9 @@
-Require Import Coq.Bool.Bool.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
-Require Import Coq.derive.Derive.
+From Coq Require Import Bool.
+From Coq Require Import ZArith.
+From Coq Require Import FMapPositive.
+From Coq Require Import MSetPositive.
+From Coq Require Import List.
+From Coq Require Import Derive.
 Require Import Rewriter.Util.CPSNotations.
 Require Import Rewriter.Util.Option.
 Require Import Rewriter.Util.PrimitiveSigma.

diff --git a/src/Rewriter/Language/IdentifiersLibraryProofs.v b/src/Rewriter/Language/IdentifiersLibraryProofs.v
@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+From Coq Require Import ZArith.
+From Coq Require Import MSetPositive.
+From Coq Require Import FMapPositive.
 Require Import Rewriter.Util.PrimitiveSigma.
 Require Import Rewriter.Util.MSetPositive.Facts.
 Require Import Rewriter.Util.CPSNotations.

diff --git a/src/Rewriter/Language/Language.v b/src/Rewriter/Language/Language.v
@@ -1,9 +1,9 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
+From Coq Require Import ZArith.
+From Coq Require Import FMapPositive.
+From Coq Require Import Bool.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq Require Import Relation_Definitions.
 Require Import Rewriter.Language.PreCommon.
 Require Import Rewriter.Util.LetIn.
 Require Import Rewriter.Util.ListUtil.

diff --git a/src/Rewriter/Language/PreLemmas.v b/src/Rewriter/Language/PreLemmas.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+From Coq Require Import List.
 Require Import Rewriter.Language.Pre.
 Require Import Rewriter.Util.Bool.
 Require Import Rewriter.Util.NatUtil.

diff --git a/src/Rewriter/Language/Reify.v b/src/Rewriter/Language/Reify.v
@@ -1,9 +1,9 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
+From Coq Require Import ZArith.
+From Coq Require Import FMapPositive.
+From Coq Require Import Bool.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq Require Import Relation_Definitions.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Printf.
 Require Import Rewriter.Language.PreCommon.

diff --git a/src/Rewriter/Language/UnderLetsProofs.v b/src/Rewriter/Language/UnderLetsProofs.v
@@ -1,6 +1,6 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq Require Import SetoidList.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.

diff --git a/src/Rewriter/Language/Wf.v b/src/Rewriter/Language/Wf.v
@@ -1,9 +1,9 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.micromega.Lia.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relations.
+From Coq Require Import ZArith.
+From Coq Require Import List.
+From Coq Require Import Lia.
+From Coq Require Import FMapPositive.
+From Coq Require Import Morphisms.
+From Coq Require Import Relations.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Util.Tactics.BreakMatch.

diff --git a/src/Rewriter/Rewriter/AllTactics.v b/src/Rewriter/Rewriter/AllTactics.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.Morphisms.
+From Coq Require Import Morphisms.
 Require Import Rewriter.Language.Pre.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.

diff --git a/src/Rewriter/Rewriter/Examples.v b/src/Rewriter/Rewriter/Examples.v
@@ -1,7 +1,7 @@
 (** * Examples of Using the Rewriter *)
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
+From Coq Require Import List.
 Require Import Rewriter.Util.ListUtil.
 Require Import Rewriter.Util.LetIn.
 Require Import Rewriter.Util.Notations.

diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v b/src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
@@ -1,10 +1,10 @@
-Require Import Coq.QArith.QArith.
-Require Import Coq.Structures.Orders.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Sorting.Mergesort.
-Require Export Coq.Lists.List.
-Require Export Coq.ZArith.ZArith.
+From Coq Require Import QArith.
+From Coq Require Import Orders.
+From Coq Require Import Lia.
+From Coq Require Import Bool.
+From Coq Require Import Mergesort.
+From Coq Require Export List.
+From Coq Require Export ZArith.
 Export ListNotations.
 
 Global Set Printing Width 1000.

diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v b/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
@@ -1,10 +1,10 @@
-Require Import Coq.Strings.String.
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.QArith.QArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Lists.List.
+From Coq Require Import String.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
+From Coq Require Import QArith.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
+From Coq Require Import List.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
 Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
 Require Rewriter.Rewriter.Examples.PerfTesting.Sample.

diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v b/src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
@@ -1,6 +1,6 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
 
 Global Instance list_rect_Proper_dep_gen {A P} (RP : forall x : list A, P x -> P x -> Prop)
   : Proper (RP nil ==> forall_relation (fun x => forall_relation (fun xs => RP xs ==> RP (cons x xs))) ==> forall_relation RP) (@list_rect A P) | 10.

diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v b/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
@@ -1,10 +1,10 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.QArith.QArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
+From Coq Require Import QArith.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
+From Coq Require Import String.
+From Coq Require Import List.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
 Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
 Require Import Rewriter.Util.plugins.RewriterBuild.
@@ -99,7 +99,7 @@ Local Instance Z_prod_has_compress : Sample.has_compress (Z * Z) Z := size_of_ar
 Local Instance Z_prod_has_make : Sample.has_make (Z * Z) Z := { make_T := invert_size_of_arg_dumb ; make_T_correct := invert_size_of_arg_dumb_correct }.
 
 Module Import instances.
-  Import Coq.QArith.QArith Coq.QArith.Qround Coq.QArith.Qabs Coq.QArith.Qminmax.
+  Import QArith Qround Qabs Qminmax.
   Import Sample.
   Local Open Scope Z_scope.
   Local Set Warnings Append "-ambiguous-paths".
@@ -421,7 +421,7 @@ Ltac describe_goal nm :=
 
 Ltac do_coq_rewrite _ := rewrite -> !Z.add_0_r.
 
-Require Import Coq.ssr.ssreflect.
+From Coq Require Import ssreflect.
 
 Ltac do_ssr_rewrite _ := rewrite !Z.add_0_r.
 

diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v b/src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
@@ -1,14 +1,14 @@
 (** Utility file for subsampling large distributions *)
-Require Import Coq.Strings.String.
-Require Import Coq.Structures.Orders.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Sorting.Mergesort.
-Require Import Coq.QArith.QArith Coq.QArith.Qround Coq.QArith.Qabs Coq.QArith.Qminmax.
-Require Import Coq.NArith.NArith.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Arith.Arith.
-Require Import Coq.Lists.List.
+From Coq Require Import String.
+From Coq Require Import Orders.
+From Coq Require Import Lia.
+From Coq Require Import Bool.
+From Coq Require Import Mergesort.
+From Coq Require Import QArith Qround Qabs Qminmax.
+From Coq Require Import NArith.
+From Coq Require Import ZArith.
+From Coq Require Import Arith.
+From Coq Require Import List.
 Require Import Rewriter.Util.LetIn.
 Import ListNotations.
 Local Open Scope list_scope.

diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v b/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
@@ -1,10 +1,10 @@
-Require Import Coq.QArith.QArith.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Export Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.Strings.String.
+From Coq Require Import QArith.
+From Coq Require Import MSetPositive.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
+From Coq Require Export ZArith.
+From Coq Require Import List.
+From Coq Require Import String.
 Require Import Rewriter.Util.Prod.
 Require Import Rewriter.Util.Bool.Reflect.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.

diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v b/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
@@ -1,10 +1,10 @@
-Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.QArith.QArith.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Lists.List.
-Require Import Coq.Strings.String.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.
+From Coq Require Import QArith.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
+From Coq Require Import List.
+From Coq Require Import String.
 Require Import Rewriter.Util.Option Rewriter.Util.Strings.ParseArithmetic.
 Require Import Rewriter.Rewriter.Examples.PerfTesting.Harness.
 Require Import Rewriter.Util.plugins.RewriterBuild.

diff --git a/src/Rewriter/Rewriter/Examples/PrefixSums.v b/src/Rewriter/Rewriter/Examples/PrefixSums.v
@@ -1,8 +1,8 @@
 (** * Examples of Using the Rewriter *)
-Require Import Coq.micromega.Lia.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Lists.List.
+From Coq Require Import Lia.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
+From Coq Require Import List.
 Require Import Rewriter.Util.LetIn.
 Require Import Rewriter.Util.Notations.
 Require Import Rewriter.Util.NatUtil.

diff --git a/src/Rewriter/Rewriter/InterpProofs.v b/src/Rewriter/Rewriter/InterpProofs.v
@@ -1,10 +1,10 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.SetoidList.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
+From Coq Require Import SetoidList.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq Require Import MSetPositive.
+From Coq Require Import FMapPositive.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.

diff --git a/src/Rewriter/Rewriter/ProofsCommon.v b/src/Rewriter/Rewriter/ProofsCommon.v
@@ -1,11 +1,11 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.SetoidList.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.Program.Tactics.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
+From Coq Require Import SetoidList.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq Require Import MSetPositive.
+From Coq Require Import FMapPositive.
+From Coq.Program Require Import Tactics.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.

diff --git a/src/Rewriter/Rewriter/ProofsCommonTactics.v b/src/Rewriter/Rewriter/ProofsCommonTactics.v
@@ -1,10 +1,10 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.SetoidList.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.FSets.FMapPositive.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
+From Coq Require Import SetoidList.
+From Coq Require Import List.
+From Coq Require Import Morphisms.
+From Coq Require Import MSetPositive.
+From Coq Require Import FMapPositive.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Rewriter.Language.Wf.

diff --git a/src/Rewriter/Rewriter/Reify.v b/src/Rewriter/Rewriter/Reify.v
@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import FMapPositive.
+From Coq Require Import MSetPositive.
+From Coq Require Import List.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Printf.
 Require Import Ltac2.Bool.

diff --git a/src/Rewriter/Rewriter/Rewriter.v b/src/Rewriter/Rewriter/Rewriter.v
@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import FMapPositive.
+From Coq Require Import MSetPositive.
+From Coq Require Import List.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.UnderLets.
 Require Import Rewriter.Language.IdentifiersLibrary.