Adapt to rocq-prover/rocq#19530

Author: proux01

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.

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

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.

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.

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.

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".

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.

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.

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.

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.