Adapt to coq/coq#19530

coq-community · Sep 17, 2024 · cbcd547 · cbcd547
1 parent 5ce96ab
commit cbcd547
Show file tree

Hide file tree

Showing 16 changed files with 35 additions and 39 deletions.
diff --git a/examples/ConsiderDemo.v b/examples/ConsiderDemo.v
@@ -1,10 +1,10 @@
-Require Import Coq.Bool.Bool.
-Require Import Arith.PeanoNat.
+From Coq Require Import Bool.
+From Coq Require Import PeanoNat.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Data.Nat.
 
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
 
 Set Implicit Arguments.
 Set Strict Implicit.

diff --git a/theories/Core/Decision.v b/theories/Core/Decision.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.DecidableClass.
+From Coq.Classes Require Import DecidableClass.
 
 Definition decideP (P : Prop) {D : Decidable P} : {P} + {~P} :=
   match @Decidable_witness P D as X return (X = true -> P) -> (X = false -> ~P) -> {P} + {~P} with

diff --git a/theories/Core/EquivDec.v b/theories/Core/EquivDec.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.EquivDec.
+From Coq.Classes Require Import EquivDec.
 
 Theorem EquivDec_refl_left {T : Type} {c : EqDec T (@eq T)} :
   forall (n : T), equiv_dec n n = left (refl_equal _).
@@ -9,4 +9,4 @@ Proof.
   reflexivity.
 Qed.
 
-Export Coq.Classes.EquivDec.
+Export EquivDec.
diff --git a/theories/Data/HList.v b/theories/Data/HList.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List Coq.Arith.PeanoNat.
+From Coq Require Import List PeanoNat.
 Require Import Relations RelationClasses.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Data.SigT.

diff --git a/theories/Data/List.v b/theories/Data/List.v
@@ -1,5 +1,4 @@
-Require Import Coq.Lists.List.
-Require Coq.Classes.EquivDec.
+From Coq Require Import List EquivDec.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Structures.Reducible.
@@ -20,7 +19,7 @@ Section EqDec.
   Proof.
     red. unfold Equivalence.equiv, RelationClasses.complement.
     intros.
-    change (x = y -> False) with (x <> y).
+    change (x = y -> False) with (not (x = y)).
     decide equality. eapply EqDec_T.
   Qed.
 End EqDec.

diff --git a/theories/Data/ListFirstnSkipn.v b/theories/Data/ListFirstnSkipn.v
@@ -1,6 +1,6 @@
-Require Import Coq.Lists.List.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
+From Coq.Lists Require Import List.
+From Coq.ZArith Require Import ZArith.
+From Coq.micromega Require Import Lia.
 
 (** For backwards compatibility with hint locality attributes. *)
 Set Warnings "-unsupported-attributes".

diff --git a/theories/Data/ListNth.v b/theories/Data/ListNth.v
@@ -1,5 +1,5 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Arith.PeanoNat.
+From Coq.Lists Require Import List.
+From Coq.Arith Require Import PeanoNat.
 
 Set Implicit Arguments.
 Set Strict Implicit.

diff --git a/theories/Data/Nat.v b/theories/Data/Nat.v
@@ -1,4 +1,4 @@
-Require Coq.Arith.Arith.
+From Coq.Arith Require Arith.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Tactics.Consider.

diff --git a/theories/Data/PreFun.v b/theories/Data/PreFun.v
@@ -1,5 +1,5 @@
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relations.
+From Coq.Classes Require Import Morphisms.
+From Coq.Relations Require Import Relations.
 
 Set Implicit Arguments.
 Set Strict Implicit.

diff --git a/theories/Data/SigT.v b/theories/Data/SigT.v
@@ -1,4 +1,4 @@
-Require Coq.Classes.EquivDec.
+From Coq.Classes Require EquivDec.
 Require Import ExtLib.Structures.EqDep.
 Require Import ExtLib.Tactics.Injection.
 Require Import ExtLib.Tactics.EqDep.

diff --git a/theories/Data/String.v b/theories/Data/String.v
@@ -1,6 +1,4 @@
-Require Import Coq.Strings.String.
-Require Import Coq.Program.Program. 
-Require Import Coq.Arith.PeanoNat.
+From Coq Require Import String Program PeanoNat.
 
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Core.RelDec.

diff --git a/theories/Programming/Show.v b/theories/Programming/Show.v
@@ -1,9 +1,8 @@
-Require Coq.Strings.Ascii.
-Require Coq.Strings.String.
-Require Import Coq.Strings.String.
-Require Import Coq.Program.Wf.
-Require Import Coq.PArith.BinPos.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Ascii.
+From Coq Require Import String.
+From Coq.Program Require Import Wf.
+From Coq Require Import BinPos.
+From Coq Require Import ZArith.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Structures.Reducible.
 Require Import ExtLib.Programming.Injection.

diff --git a/theories/Recur/Measure.v b/theories/Recur/Measure.v
@@ -1,5 +1,5 @@
-Require Import Coq.Classes.RelationClasses.
-Require Coq.Arith.Wf_nat.
+From Coq.Classes Require Import RelationClasses.
+From Coq.Arith Require Wf_nat.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -34,4 +34,4 @@ Section measure.
 
   Definition well_founded_mlt : well_founded mlt :=
     @well_founded_compose T nat m lt Wf_nat.lt_wf.
-End measure.
+End measure.
diff --git a/theories/Structures/EqDep.v b/theories/Structures/EqDep.v
@@ -1,4 +1,4 @@
-Require Coq.Logic.Eqdep_dec.
+From Coq.Logic Require Eqdep_dec.
 Require EquivDec.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Tactics.Consider.
@@ -12,18 +12,18 @@ Section Classes.
 
   Theorem UIP_refl : forall {x : A} (p1 : x = x), p1 = refl_equal _.
     intros.
-    eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
+    eapply Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
   Qed.
 
   Theorem UIP_equal : forall {x y : A} (p1 p2 : x = y), p1 = p2.
-    eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
+    eapply Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
   Qed.
 
   Lemma inj_pair2 :
     forall (P:A -> Type) (p:A) (x y:P p),
       existT P p x = existT P p y -> x = y.
   Proof.
-    intros. eapply Coq.Logic.Eqdep_dec.inj_pair2_eq_dec; auto.
+    intros. eapply Eqdep_dec.inj_pair2_eq_dec; auto.
   Qed.
 
   Theorem equiv_dec_refl_left : forall a, @EquivDec.equiv_dec _ _ _ dec a a = left eq_refl.

diff --git a/theories/Structures/FunctorLaws.v b/theories/Structures/FunctorLaws.v
@@ -1,4 +1,4 @@
-Require Import Coq.Relations.Relations.
+From Coq.Relations Require Import Relations.
 Require Import ExtLib.Data.Fun.
 Require Import ExtLib.Structures.Functor.
 

diff --git a/theories/Tactics/EqDep.v b/theories/Tactics/EqDep.v
@@ -1,6 +1,6 @@
-Require Import Coq.Classes.EquivDec.
+From Coq.Classes Require Import EquivDec.
 Require Import ExtLib.Structures.EqDep.
-Require Coq.Logic.Eqdep_dec.
+From Coq.Logic Require Eqdep_dec.
 
 Set Implicit Arguments.
 Set Strict Implicit.