Merge pull request #616 from proux01/stdlib_repo

Adapt to coq/coq#19530

examples/Fin.v

@@ -8,7 +8,7 @@
 
 (** An example development of the [fin] datatype using [equations]. *)
 
-Require Import Program.Basics Program.Combinators.
+From Coq.Program Require Import Basics Combinators.
 From Equations Require Import Equations.
 Open Scope equations_scope.
 (** [fin n] is the type of naturals smaller than [n]. *)

examples/POPLMark1a.v

@@ -6,7 +6,7 @@
 
 Require Import Program.
 From Equations Require Import Equations.
-Require Import Stdlib.Classes.EquivDec.
+From Stdlib Require Import EquivDec.
 Require Import Arith.
 
 Definition scope := nat.

examples/accumulator.v

@@ -16,7 +16,7 @@
   recursion and function eliminators. *)
 
 From Equations Require Import Equations.
-From Stdlib Require Import List Program.Syntax Arith Lia.
+From Stdlib Require Import List Syntax Arith Lia.
 Import ListNotations.
 
 (** ** Worker/wrapper

examples/mutualwfrec.v

@@ -8,7 +8,7 @@
 (**********************************************************************)
 
 From Equations Require Import Equations.
-From Stdlib Require Import List Program.Syntax Arith Lia.
+From Stdlib Require Import List Syntax Arith Lia.
 Require Import List Wellfounded.
 Import ListNotations.
 (* end hide *)

examples/ordinals.v

@@ -1,6 +1,6 @@
 Require Import Arith.
-Require Import Stdlib.Logic.Eqdep_dec.
-Require Import Stdlib.Arith.Peano_dec.
+From Stdlib Require Import Eqdep_dec.
+From Stdlib Require Import Peano_dec.
 Require Import List.
 Require Import Recdef.
 

examples/string_matching.v

@@ -1,8 +1,8 @@
 (** Example by Nicky Vazou, unfinished *)
 
 Require Import Arith.
-Require Import Stdlib.Classes.DecidableClass.
-Require Import Stdlib.Program.Wf.
+From Stdlib Require Import DecidableClass.
+From Stdlib.Program Require Import Wf.
 Require Import List Lia.
 Require Import PeanoNat.
 Require Import Program.

examples/views.v

@@ -9,7 +9,7 @@
 (* end hide *)
 
 From Equations Require Import Equations.
-From Stdlib Require Import List Program.Syntax Arith Lia.
+From Stdlib Require Import List Syntax Arith Lia.
 
 (** * Views using dependent pattern-matching
 
@@ -107,4 +107,4 @@ Goal forall n, n <> 10 -> f n = n + 1.
   intros n; apply f_elim'.
  (* 2 cases: 10 and not 10 *)
   all:simpl; congruence.
-Qed.
+Qed.

examples/wfrec.v

@@ -8,7 +8,7 @@
 (**********************************************************************)
 
 From Equations Require Import Equations.
-From Stdlib Require Import List Program.Syntax Arith Lia.
+From Stdlib Require Import List Syntax Arith Lia.
 Require Import List.
 Import ListNotations.
 (* end hide *)

test-suite/eqdec_error.v

@@ -1,4 +1,4 @@
-Require Import Stdlib.Numbers.BinNums.
+From Stdlib Require Import BinNums.
 
 From Equations Require Import Equations.
 

test-suite/issues/issue120.v

@@ -1,7 +1,7 @@
 Require Export Lia.
 From Equations Require Import Equations.
-Require Import Stdlib.Relations.Relation_Operators.
-Require Import Stdlib.Wellfounded.Lexicographic_Product.
+From Stdlib Require Import Relation_Operators.
+From Stdlib Require Import Lexicographic_Product.
 
 Inductive id : Type := Id : nat -> id.
 Inductive var : Type :=

test-suite/issues/issue228.v

@@ -1,7 +1,7 @@
-Require Import Unicode.Utf8.
-Require Import Program.Equality.
-Require Import Arith.
-Require Vectors.Vector.
+From Coq Require Import Utf8.
+From Coq Require Import Equality.
+From Coq Require Import Arith.
+From Coq Require Vector.
 Import Vector.VectorNotations.
 From Equations Require Import Equations.
 

test-suite/issues/issue353.v

@@ -1,4 +1,4 @@
-Require Import Stdlib.Arith.Arith.
+From Stdlib Require Import Arith.
 From Equations Require Import Equations.
 
 Fixpoint Ack (n m : nat) : nat :=

test-suite/rec.v

@@ -58,10 +58,10 @@ Section Nested.
 
 End Nested.
 
-Require Import Stdlib.Lists.SetoidList.
-Require Import Stdlib.Sorting.Sorting.
-Require Import Stdlib.Sorting.Permutation.
-Require Import Stdlib.Sorting.PermutSetoid.
+From Stdlib Require Import SetoidList.
+From Stdlib Require Import Sorting.
+From Stdlib Require Import Permutation.
+From Stdlib Require Import PermutSetoid.
 
 #[export]
 Instance filter_ext {A} : Morphisms.Proper (pointwise_relation A eq ==> eq ==> eq) (@filter A).

test-suite/scope.v

@@ -4,8 +4,8 @@
 Require Import Program.
 Require Import Equations.Prop.DepElim.
 Require Import Equations.Prop.Equations.
-Require Import Stdlib.Logic.Eqdep_dec.
-Require Import Stdlib.Classes.EquivDec.
+From Stdlib Require Import Eqdep_dec.
+From Stdlib Require Import EquivDec.
 
 Require Import Arith.
 Derive Signature for eq.

theories/Prop/Constants.v

@@ -52,7 +52,7 @@ Register Init.Datatypes.pair as equations.product.intro.
 Register Classes.WellFounded as equations.wellfounded.class.
 Register Init.Wf.well_founded as equations.wellfounded.type.
 Register Relations.Relation_Definitions.relation as equations.relation.type.
-Register Relations.Relation_Operators.clos_trans as equations.relation.transitive_closure.
+Register Relation_Operators.clos_trans as equations.relation.transitive_closure.
 
 (* Dependent elimination constants *)
 Register Equations.Prop.DepElim.solution_left as equations.depelim.solution_left.