Adapt to coq/coq#19530 (#47)

coq-community · Sep 21, 2024 · d9d85c8 · d9d85c8
1 parent c0b15f5
commit d9d85c8
Show file tree

Hide file tree

Showing 28 changed files with 79 additions and 79 deletions.
diff --git a/PerformanceExperiments/Harness.v b/PerformanceExperiments/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.
 Require Import PerformanceExperiments.Sandbox.
 Export ListNotations.
 

diff --git a/PerformanceExperiments/LetIn.v b/PerformanceExperiments/LetIn.v
@@ -1,5 +1,5 @@
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
 
 Reserved Notation "'dlet' x .. y := v 'in' f"
          (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").

diff --git a/PerformanceExperiments/ListRectInstances.v b/PerformanceExperiments/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/PerformanceExperiments/PrimitiveProd.v b/PerformanceExperiments/PrimitiveProd.v
@@ -1,5 +1,5 @@
 (** * Define a primitive pairing type *)
-Require Import Coq.Classes.Morphisms.
+From Coq Require Import Morphisms.
 
 Local Set Primitive Projections.
 

diff --git a/PerformanceExperiments/Reify/BenchmarkExtraUtil.v b/PerformanceExperiments/Reify/BenchmarkExtraUtil.v
@@ -1,5 +1,5 @@
-Require Import Coq.Lists.List.
-Require Import Coq.NArith.NArith.
+From Coq Require Import List.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Sandbox.
 Require Import Reify.ReifyCommon.
 Require Import Reify.PHOASUtil.

diff --git a/PerformanceExperiments/Reify/BenchmarkUtil.v b/PerformanceExperiments/Reify/BenchmarkUtil.v
@@ -1,5 +1,5 @@
 (** * Various utilities for benchmarking *)
-Require Import Coq.NArith.NArith. (* for Pos.iter_op and Z.of_nat *)
+From Coq Require Import NArith. (* for Pos.iter_op and Z.of_nat *)
 Require Import Reify.Common.
 Require Reify.PHOAS.
 Require Import Reify.PHOASUtil.

diff --git a/PerformanceExperiments/Reify/CanonicalStructures.v b/PerformanceExperiments/Reify/CanonicalStructures.v
@@ -1,7 +1,7 @@
 (** * Canonical-structure based reification *)
 Require Import Reify.ReifyCommon.
-Require Import Coq.Lists.List.
-Require Import Coq.NArith.NArith.
+From Coq Require Import List.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 Require Import Reify.CanonicalStructuresReifyCommon.

diff --git a/PerformanceExperiments/Reify/Ltac2.v b/PerformanceExperiments/Reify/Ltac2.v
@@ -1,6 +1,6 @@
 (** * Reification by Ltac2 *)
 Require Import Reify.ReifyCommon.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.Ltac2Reify.
 Require Import Reify.BenchmarkExtraUtil.

diff --git a/PerformanceExperiments/Reify/LtacVariants.v b/PerformanceExperiments/Reify/LtacVariants.v
@@ -1,5 +1,5 @@
 (** * Ltac-based reification, using uncurrying to reucurse under binders *)
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 Require

diff --git a/PerformanceExperiments/Reify/OCaml.v b/PerformanceExperiments/Reify/OCaml.v
@@ -1,7 +1,7 @@
 (** * Reification in OCaml *)
 Require Import Reify.ReifyCommon.
 Require Import Reify.OCamlReify.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 (** See [OCamlReify.v] and [reify_plugin.{ml4,mlg}] for the implementation code. *)

diff --git a/PerformanceExperiments/Reify/Parametricity.v b/PerformanceExperiments/Reify/Parametricity.v
@@ -1,6 +1,6 @@
 (** * Reification by parametricity *)
 Require Import Reify.ReifyCommon.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.ParametricityCommon.
 Require Import Reify.BenchmarkExtraUtil.

diff --git a/PerformanceExperiments/Reify/QuoteFlat.v b/PerformanceExperiments/Reify/QuoteFlat.v
@@ -1,7 +1,7 @@
 (** * Reification by the quote plugin *)
-Require Import Coq.quote.Quote.
+From Coq Require Import Quote.
 Require Import Reify.ReifyCommon.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 

diff --git a/PerformanceExperiments/Reify/TypeClasses.v b/PerformanceExperiments/Reify/TypeClasses.v
@@ -1,6 +1,6 @@
 (** * Typeclass-based reification *)
 Require Import Reify.ReifyCommon.
-Require Import Coq.NArith.NArith.
+From Coq Require Import NArith.
 Require Import PerformanceExperiments.Harness.
 Require Import Reify.BenchmarkExtraUtil.
 

diff --git a/PerformanceExperiments/Sample.v b/PerformanceExperiments/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 PerformanceExperiments.LetIn.
 Import ListNotations.
 Local Open Scope list_scope.

diff --git a/PerformanceExperiments/n_polymorphic_universes.v b/PerformanceExperiments/n_polymorphic_universes.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import PerformanceExperiments.Harness.
 Global Open Scope Z_scope.
 Set Universe Polymorphism.

diff --git a/PerformanceExperiments/rewrite_lift_lets_map.v b/PerformanceExperiments/rewrite_lift_lets_map.v
@@ -1,9 +1,9 @@
-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 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 PerformanceExperiments.Harness.
 Require PerformanceExperiments.Sample.
 Require Export PerformanceExperiments.LetIn PerformanceExperiments.ListRectInstances.

diff --git a/PerformanceExperiments/rewrite_plus_0_tree.v b/PerformanceExperiments/rewrite_plus_0_tree.v
@@ -1,9 +1,9 @@
-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 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 PerformanceExperiments.Harness.
 Require PerformanceExperiments.Sample.
 Import ListNotations.
@@ -91,7 +91,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".
@@ -346,7 +346,7 @@ Hint Rewrite Z.add_0_r : mydb.
 
 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/PerformanceExperiments/rewrite_repeated_app_autorewrite_noop.v b/PerformanceExperiments/rewrite_repeated_app_autorewrite_noop.v
@@ -20,7 +20,7 @@ Ltac do_rewrite_ques := try rewrite ?fg.
 Ltac do_rewrite_bang_evar := try rewrite !(fg _).
 Ltac do_rewrite_once_evar := try rewrite (fg _).
 Ltac do_rewrite_ques_evar := try rewrite ?(fg _).
-Require Import Coq.ssr.ssreflect.
+From Coq Require Import ssreflect.
 Ltac do_ssr_rewrite_bang := try rewrite !fg.
 Ltac do_ssr_rewrite_once := try rewrite fg.
 Ltac do_ssr_rewrite_ques := try rewrite ?fg.

diff --git a/PerformanceExperiments/rewrite_repeated_app_common.v b/PerformanceExperiments/rewrite_repeated_app_common.v
@@ -1,5 +1,5 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+From Coq Require Import ZArith.
+From Coq Require Import Setoid Morphisms.
 Local Open Scope core_scope.
 Axiom f : nat -> nat.
 Axiom g : nat -> nat.

diff --git a/PerformanceExperiments/rewrite_repeated_app_common_ltac2.v b/PerformanceExperiments/rewrite_repeated_app_common_ltac2.v
@@ -1,4 +1,4 @@
-Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+From Coq Require Import Setoid Morphisms.
 Require Export PerformanceExperiments.rewrite_repeated_app_common.
 Require Import Ltac2.Ltac2.
 Require Import Ltac2.Constr.

diff --git a/PerformanceExperiments/rewrite_repeated_app_ssrrewrite.v b/PerformanceExperiments/rewrite_repeated_app_ssrrewrite.v
@@ -12,7 +12,7 @@ Definition args_of_size (s : size) : list nat
      | VerySlow => []
      end.
 
-Require Import Coq.ssr.ssreflect.
+From Coq Require Import ssreflect.
 
 Ltac do_rewrite := rewrite !fg.
 

diff --git a/PerformanceExperiments/rewrite_repeated_app_ssrrewrite_noop.v b/PerformanceExperiments/rewrite_repeated_app_ssrrewrite_noop.v
@@ -1,4 +1,4 @@
-Require Export Coq.ZArith.ZArith.
+From Coq Require Export ZArith.
 Require Import PerformanceExperiments.Harness.
 Require Export PerformanceExperiments.rewrite_repeated_app_common.
 
@@ -12,7 +12,7 @@ Definition args_of_size (s : size) : list nat
      | VerySlow => []
      end.
 
-Require Import Coq.ssr.ssreflect.
+From Coq Require Import ssreflect.
 Ltac do_ssr_rewrite_bang := try rewrite !f'g'.
 Ltac do_ssr_rewrite_once := try rewrite f'g'.
 Ltac do_ssr_rewrite_ques := try rewrite ?f'g'.

diff --git a/PerformanceExperiments/rewrite_under_binders_common.v b/PerformanceExperiments/rewrite_under_binders_common.v
@@ -1,6 +1,6 @@
 (** * performance of rewrite/rewrite_strat under binders *)
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
+From Coq Require Import Morphisms.
+From Coq Require Import Setoid.
 
 Module Type LetInT.
   Parameter Let_In : forall {A P} (x : A) (f : forall a : A, P a), P x.

diff --git a/PerformanceExperiments/rewrite_under_lets_plus_0.v b/PerformanceExperiments/rewrite_under_lets_plus_0.v
@@ -1,9 +1,9 @@
-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 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 PerformanceExperiments.Harness.
 Require PerformanceExperiments.Sample.
 Require Export PerformanceExperiments.LetIn PerformanceExperiments.ListRectInstances.

diff --git a/PerformanceExperiments/sieve_of_eratosthenes.v b/PerformanceExperiments/sieve_of_eratosthenes.v
@@ -1,9 +1,9 @@
-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.
+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.
 Require Import PerformanceExperiments.Harness.
 Require PerformanceExperiments.Sample.
 Import ListNotations.

diff --git a/src/Nia.v b/src/Nia.v
@@ -1,6 +1,6 @@
 (* -*- coqchk-prog-args: ("-bytecode-compiler" "yes") -*- *)
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
 Open Scope Z_scope.
 
 (** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this

diff --git a/src/fiat_crypto_via_setoid_rewrite_standalone.v b/src/fiat_crypto_via_setoid_rewrite_standalone.v
@@ -1,8 +1,8 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround.
+From Coq Require Import ZArith.
+From Coq Require Import List.
+From Coq Require Import Setoid.
+From Coq Require Import Morphisms.
+From Coq Require Import QArith_base Qreduction Qround.
 Import List.ListNotations.
 Local Open Scope Z_scope.
 Local Open Scope list_scope.

diff --git a/src/n_polymorphic_universes.v b/src/n_polymorphic_universes.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Local Open Scope Z_scope.
 Set Universe Polymorphism.
 Record prod A B := pair { fst : A ; snd : B }.