diff --git a/doc/equations_intro.v b/doc/equations_intro.v
index 3b89cfb30..b01e11ea9 100644
--- a/doc/equations_intro.v
+++ b/doc/equations_intro.v
@@ -16,7 +16,7 @@ From Equations.Prop Require Import Equations.
 
 (* begin hide *)
 Check @eq.
-Require Import Bvector.
+From Stdlib Require Import Bvector.
 
 (* Derive DependentElimination for nat bool option sum Datatypes.prod list *)
 (* end hide *)
diff --git a/dune-project b/dune-project
index 52beb40c6..22584373a 100644
--- a/dune-project
+++ b/dune-project
@@ -25,10 +25,14 @@
    (ppx_optcomp :build)
    (ocaml-lsp-server :with-dev-setup)))
 
+(package
+ (name rocq-equations-examples)
+ (synopsis "Examples")
+ (description "Do not install")
+ (depends rocq-equations))
+
 (package
  (name rocq-equations-tests)
  (synopsis "Technical package to run tests")
  (description "Do not install")
  (depends rocq-equations))
-
-(generate_opam_files)
\ No newline at end of file
diff --git a/examples/AlmostFull.v b/examples/AlmostFull.v
index 50c639d7e..e3a853184 100644
--- a/examples/AlmostFull.v
+++ b/examples/AlmostFull.v
@@ -1,17 +1,20 @@
 From Equations.Prop Require Import Equations.
 
 Require Import Examples.Fin.
-Require Import Relations Utf8.
-Require Import Relations Wellfounded.
-Require Import Setoid RelationClasses Morphisms.
-Require Import Lia.
-Require Import Bool.
-Require Import List Arith String.
+From Stdlib Require Import Relations Utf8.
+From Stdlib Require Import Relations Wellfounded.
+From Stdlib Require Import Setoid RelationClasses Morphisms.
+From Stdlib Require Import Lia.
+From Stdlib Require Import Bool.
+From Stdlib Require Import List Arith String.
 From Stdlib Require Import FunctionalExtensionality.
 
 Set Equations Transparent.
 Set Keyed Unification.
 Set Asymmetric Patterns.
+Local Set Firstorder Solver auto with arith core datatypes.
+
+Ltac intuition_solver ::= auto with *.
 
 Section Equality.
   Class Eq (A : Type) :=
@@ -449,7 +452,7 @@ Section OplusUnary.
 
 End OplusUnary.
 
-Set Firstorder Solver auto.
+Local Set Firstorder Solver auto.
 
 (* Lemma oplus_unary_sec_intersection {X} (p q : WFT X) *)
 (*       (C : X -> X -> Prop) (A B : X -> Prop) : *)
@@ -610,7 +613,7 @@ Ltac destruct_pairs := repeat
   | [ x : _ /\ _ |- _ ] => destruct x
 end.
 
-Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 
 Section SCT.
 
@@ -1353,7 +1356,7 @@ Print Assumptions size_change_wf.
 Print Assumptions size_change_termination.
 
 Definition R := product_rel Nat.le Nat.le.
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 Derive Signature for clos_trans_1n.
 
@@ -1391,7 +1394,7 @@ Definition gnlex : (nat * nat) -> nat.
   red. simpl. red. compute. simpl. intuition lia. red. simpl. compute. intuition lia.
 Defined.
 
-Require Import ExtrOcamlBasic.
+From Stdlib Require Import ExtrOcamlBasic.
 (* Extraction gnlex.
 Print Assumptions gnlex. *)
 
diff --git a/examples/Basics.v b/examples/Basics.v
index 1babe7ada..5c53fe0a3 100644
--- a/examples/Basics.v
+++ b/examples/Basics.v
@@ -22,9 +22,10 @@
   If running this interactively you can ignore the printing
   and hide directives which are just used to instruct coqdoc. *)
 
-Require Import Program Bvector List Relations.
+#[warnings="-deprecated-library-file-since-8.20"]
+From Stdlib Require Import Program Bvector List Relations.
 From Equations Require Import Equations Signature.
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 
 Set Keyed Unification.
 
@@ -65,7 +66,7 @@ app_with (cons a v) l with app_with v l => {
 (** Structurally recursive function on natural numbers, with inspection of a recursive
     call result. We use [auto with arith] to discharge the obligations. *)
 
-Obligation Tactic := program_simpl ; try CoreTactics.solve_wf ; auto with arith.
+Local Obligation Tactic := program_simpl ; try CoreTactics.solve_wf ; auto with arith.
 
 Equations equal (n m : nat) : { n = m } + { n <> m } :=
 equal O O := in_left ;
@@ -152,7 +153,7 @@ sublist p (cons x xs) with p x := {
 
 (** Well-founded definitions: *)
 
-Require Import Arith Wf_nat.
+From Stdlib Require Import Arith Wf_nat.
 
 (** One can declare new well-founded relations using instances of the [WellFounded] typeclass. *)
 #[local] Instance wf_nat : WellFounded lt := lt_wf.
@@ -230,6 +231,7 @@ Equations app {A} (l l' : list A) : list A :=
 app nil l := l;
 app (cons a v) l := cons a (app v l).
 
+#[warnings="-notation-overridden"]
 Infix "++" := app (right associativity, at level 60) : list_scope.
 
 Equations rev_acc {A} (l : list A) (acc : list A) : list A :=
@@ -336,7 +338,8 @@ Qed.
 
 (* Eval compute in @zip''. *)
 
-Require Import Bvector.
+#[warnings="-deprecated-library-file-since-8.20"]
+From Stdlib Require Import Bvector.
 
 (** This function can also be defined by structural recursion on [m]. *)
 
diff --git a/examples/Equations_Tutorial_VeriMag.v b/examples/Equations_Tutorial_VeriMag.v
index 5a3d34ef4..f457c6cfb 100644
--- a/examples/Equations_Tutorial_VeriMag.v
+++ b/examples/Equations_Tutorial_VeriMag.v
@@ -13,9 +13,10 @@
 (** printing <=? %$\le?$% *)
 (* begin hide *)
 
+Set Warnings "-undo-batch-mode".
 Set Warnings "-notation-overridden".
-Require Import Utf8 Arith Compare_dec List Lia.
-Require Import Relation_Operators Program.
+From Stdlib Require Import Utf8 Arith Compare_dec List Lia.
+From Stdlib Require Import Relation_Operators Program.
 
 Close Scope program_scope.
 Close Scope list_scope.
@@ -128,6 +129,7 @@ Module BuildingUp.
 (** Equations naturally supports notations: the left-hand 
   sides of clauses only have to be elaborated to well-typed patterns for the given argument types. *)
 
+Declare Scope mylist_scope.
 Notation "[]" := nil : mylist_scope.
 Notation "[ x ]" := (cons x nil) : mylist_scope.
 Notation "x :: l" := (cons x l) : mylist_scope.
diff --git a/examples/Fin.v b/examples/Fin.v
index a1a839a06..ef613f492 100644
--- a/examples/Fin.v
+++ b/examples/Fin.v
@@ -8,7 +8,7 @@
 
 (** An example development of the [fin] datatype using [equations]. *)
 
-From Coq.Program Require Import Basics Combinators.
+From Stdlib.Program Require Import Basics Combinators.
 From Equations.Prop Require Import Equations.
 Open Scope equations_scope.
 (** [fin n] is the type of naturals smaller than [n]. *)
@@ -78,7 +78,8 @@ Scheme finle_ind_dep := Induction for finle Sort Prop.
 
 Arguments finle {n}.
 
-Require Vectors.Vector.
+#[warnings="-warn-library-file-stdlib-vector"]
+From Stdlib Require Vectors.Vector.
 Arguments Vector.nil {A}.
 Arguments Vector.cons {A} _ {n}.
 Notation vnil := Vector.nil.
diff --git a/examples/HoTT_light.v b/examples/HoTT_light.v
index f163f65e6..089eb44e4 100644
--- a/examples/HoTT_light.v
+++ b/examples/HoTT_light.v
@@ -11,9 +11,8 @@
  ** A lightweight version of the Homotopy Type Theory library prelude. *)
 Set Warnings "-notation-overridden".
 
-Require Export Unicode.Utf8.
-Require Import Stdlib.Program.Tactics Setoid.
-Require Import Relations.
+From Stdlib Require Export Unicode.Utf8.
+From Stdlib Require Import Program.Tactics Setoid Relations.
 (** Switches to constants in Type *)
 From Equations.Type Require Import All.
 
@@ -31,7 +30,7 @@ Set Implicit Arguments.
 (** Redefine a polymorphic identity function *)
 Definition id {A : Type} (a : A) : A := a.
 
-Require Import CRelationClasses CMorphisms.
+From Stdlib Require Import CRelationClasses CMorphisms.
 
 #[local] Instance id_reflexive A : Reflexive (@Id A).
 Proof. exact (@id_refl A). Defined.
@@ -67,7 +66,9 @@ Notation "p # x" := (transport _ p x) (right associativity, at level 65, only pa
 Notation "1" := id_refl : equations_scope.
 
 (** Notation for the inverse *)
-Reserved Notation "p ^" (at level 3, format "p '^'").
+#[warnings="-notation-incompatible-prefix"]
+Reserved Notation "p ^" (at level 1, format "p '^'").
+#[warnings="-notation-incompatible-prefix"]
 Notation "p ^" := (id_sym p%equations) : equations_scope.
 
 Equations apd {A} {B : A -> Type} (f : forall x : A, B x) {x y : A} (p : x = y) :
diff --git a/examples/MoreDep.v b/examples/MoreDep.v
index fa8df0ee2..7ace00157 100644
--- a/examples/MoreDep.v
+++ b/examples/MoreDep.v
@@ -3,7 +3,7 @@
   Porting a chapter of Adam Chlipala's Certified Programming with Dependent Types,
   #<a href="http://adam.chlipala.net/cpdt/html/MoreDep.html">More Dependent Types</a>#. *)
 
-Require Import Bool Arith List Program. 
+From Stdlib Require Import Bool Arith List Program. 
 From Equations.Prop Require Import Equations.
 Set Equations Transparent.
 
@@ -101,7 +101,7 @@ pairOut _ => None.
 
 Set Printing Depth 1000000.
 
-Require Import Wellfounded.
+From Stdlib Require Import Wellfounded.
 
 Equations cfold {t} (e : exp t) : exp t :=
 (* Works with well-foundedness too: cfold e by wf (signature_pack e) exp_subterm := *)
@@ -147,7 +147,7 @@ Inductive rbtree : color -> nat -> Set :=
 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
 Derive Signature NoConfusion for rbtree.
 
-Require Import Arith Lia.
+From Stdlib Require Import Arith Lia.
 
 Section depth.
   Variable f : nat -> nat -> nat.
diff --git a/examples/POPLMark1a.v b/examples/POPLMark1a.v
index f5bb7156a..33e1b69e4 100644
--- a/examples/POPLMark1a.v
+++ b/examples/POPLMark1a.v
@@ -4,10 +4,10 @@
   inductive definition of scope and well-scoped variables (and terms,
   types and environments). *)
 
-Require Import Program.
+From Stdlib Require Import Program.
 From Equations.Prop Require Import Equations.
 From Stdlib Require Import EquivDec.
-Require Import Arith.
+From Stdlib Require Import Arith.
 
 Definition scope := nat.
 Inductive var : scope -> Set :=
diff --git a/examples/RoseTree.v b/examples/RoseTree.v
index fb52fee8c..1357bbd8d 100644
--- a/examples/RoseTree.v
+++ b/examples/RoseTree.v
@@ -6,12 +6,12 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-Require Import Program.
+From Stdlib Require Import Program.
 From Equations.Prop Require Import Equations.
 
-Require Import Utf8 Lia Arith.
+From Stdlib Require Import Utf8 Lia Arith.
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 Set Keyed Unification.
diff --git a/examples/STLC.v b/examples/STLC.v
index 47fad9a94..ec5cb0a3a 100644
--- a/examples/STLC.v
+++ b/examples/STLC.v
@@ -14,12 +14,9 @@
   well-founded order on typable terms and conclude with a normalizer building
   beta-short eta-long normal forms, typable in a bidirectional type system. *)
 
-Require Program.
+From Stdlib Require Program.
 From Equations.Prop Require Import Equations.
-
-Require Import Lia.
-Require Import List Utf8.
-
+From Stdlib Require Import Lia List Utf8.
 Import ListNotations.
 
 Set Keyed Unification.
@@ -43,6 +40,7 @@ Delimit Scope term_scope with term.
 Bind Scope term_scope with term.
 
 Notation " @( f , x ) " := (App (f%term) (x%term)).
+#[warnings="-notation-incompatible-prefix"]
 Notation " 'λ' t " := (Lambda (t%term)) (at level 10).
 Notation " << t , u >> " := (Pair (t%term) (u%term)).
 
@@ -62,7 +60,7 @@ Coercion atom : atomic_type >-> type.
 Notation " x × y " := (product x y) (at level 90).
 Notation " x ---> y " := (arrow x y) (at level 30).
 
-Require Import Arith.
+From Stdlib Require Import Arith.
 
 Equations lift (k n : nat) (t : term) : term :=
 lift k n (Var i) with Nat.compare i k := {
@@ -104,7 +102,7 @@ Proof.
   funelim (lift k 0 t); term || rewrite ?H; crush.
 Qed.
 #[local] Hint Rewrite lift0 : lift.
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 Lemma lift_k_lift_k k n m t : lift k n (lift k m t) = lift k (n + m) t.
 Proof.
@@ -165,6 +163,7 @@ where "Γ |-- i : A " := (types Γ i A).
 
 Derive Signature for types.
 
+#[warnings="-notation-incompatible-prefix"]
 Notation " [ t ] u " := (subst 0 u t) (at level 10).
 
 Notation " x @ y " := (app x y) (at level 30, right associativity).
@@ -287,12 +286,12 @@ Inductive reduce : term -> term -> Prop :=
 where " t --> u " := (reduce t u). 
 Derive Signature for reduce.
 
-Require Import Relations.
+From Stdlib Require Import Relations.
 
 Definition reduces := clos_refl_trans term reduce.
 Notation " t -->* u " := (reduces t u) (at level 55).
 
-Require Import Setoid.
+From Stdlib Require Import Setoid.
 
 #[local]
 Instance: Transitive reduces.
@@ -545,7 +544,7 @@ Proof. intros. now apply eta_expand in H0; term. Qed.
 
 (** Going to use the subterm order *)
 
-Require Import Arith Wf_nat.
+From Stdlib Require Import Arith Wf_nat.
 #[export] Instance wf_nat : Classes.WellFounded lt := lt_wf.
 
 #[local] Hint Constructors Subterm.lexprod : subterm_relation.
@@ -721,7 +720,7 @@ Proof.
   (* Lt *)
   apply Nat.compare_lt_iff in Heq. depelim H0.
   replace (nth i (Γ' @ (_ :: Γ)) unit) with (nth i (Γ' @ Γ) unit).
-  constructor. rewrite app_length. auto with arith.
+  constructor. rewrite length_app. auto with arith.
   now do 2 rewrite <- nth_extend_right by auto. 
   
   (* Gt *)
@@ -784,7 +783,7 @@ Proof.
     intros Ht2; subst t. simpl in *. depelim H0.
     specialize (Hind _ _ H H0); eauto. now apply pair_elim_snd with A0.
 Qed.
-Print Assumptions hereditary_subst_type.
+(* Print Assumptions hereditary_subst_type. *)
 Import Program.Basics.
 #[export] Instance: subrelation eq (flip impl).
 Proof. reduce. subst; auto. Qed.
@@ -856,18 +855,18 @@ Proof.
     split; intros Hsyn; depelim Hsyn;
     [depelim H1;constructor;auto|];
     (rewrite nth_app_l by lia; rewrite <- nth_app_l with (l':=Γ) by lia;
-     constructor; rewrite app_length; auto with arith). 
+     constructor; rewrite length_app; auto with arith). 
   
   (* Gt *)
   - apply Nat.compare_gt_iff in Heq.
     split; intros Hsyn; depelim Hsyn.
     depelim H1. constructor. auto.
     replace (nth i (Γ' @ (A :: Γ)) unit) with (nth (pred i) (Γ' @ Γ) unit).
-    constructor. rewrite app_length in *. simpl in H1. lia.
+    constructor. rewrite length_app in *. simpl in H1. lia.
     now apply nth_pred.
 
     replace (nth _ (Γ' @ (_ :: _)) unit) with (nth (pred i) (Γ' @ Γ) unit).
-    constructor. rewrite app_length in *. simpl in H0. lia.
+    constructor. rewrite length_app in *. simpl in H0. lia.
     now apply nth_pred.
 
   (* App *)
@@ -1003,7 +1002,7 @@ Proof.
     split; auto. intros H1. depelim H1. term. 
 Qed.
 
-Print Assumptions hereditary_subst_subst.
+(* Print Assumptions hereditary_subst_subst. *)
 
 Lemma check_liftn {Γ Γ' t T} : Γ |-- t <= T -> Γ' @ Γ |-- lift 0 (length Γ') t <= T.
 Proof. intros. apply (check_lift Γ t T [] H Γ'). Qed.
@@ -1054,4 +1053,4 @@ Proof. induction 1. (* eta-exp *)
   depelim H0.
 Qed.
 
-Print Assumptions types_normalizes.
+(* Print Assumptions types_normalizes. *)
diff --git a/examples/accumulator.v b/examples/accumulator.v
index c414678cd..eddfc8361 100644
--- a/examples/accumulator.v
+++ b/examples/accumulator.v
@@ -70,7 +70,7 @@ Qed.
 
  *)
 
-Obligation Tactic := idtac.
+Local Obligation Tactic := idtac.
 
 Equations? isPrime (n : nat) : bool :=
   isPrime 0 := false;
diff --git a/examples/bove_capretta.v b/examples/bove_capretta.v
index e8b924859..534ba1507 100644
--- a/examples/bove_capretta.v
+++ b/examples/bove_capretta.v
@@ -7,7 +7,7 @@
 
 From Equations.Prop Require Import Equations.
 
-Require Import Arith Lia Relations Utf8.
+From Stdlib Require Import Arith Lia Relations Utf8.
 Import Sigma_Notations.
 
 (** The graph of the [f91] function. *)
diff --git a/examples/definterp.v b/examples/definterp.v
index a533e7c2e..8725f46fc 100644
--- a/examples/definterp.v
+++ b/examples/definterp.v
@@ -22,11 +22,12 @@
   store extension is resolved using type class resolution as well as the
   dependent-passing style version. *)
 
-Require Import Program.Basics Program.Tactics.
+From Stdlib Require Import Program.Basics Program.Tactics.
+#[warnings="-warn-library-file-stdlib-vector"]
 Require Import Stdlib.Vectors.VectorDef.
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 From Equations.Prop Require Import Equations.
 
 Set Warnings "-notation-overridden".
@@ -332,7 +333,7 @@ Definition neg : Expr [] (bool ⇒ bool) :=
 
 Definition letref {t u} (v : Expr [] t) (b : Expr [ref t] u) : Expr [] u :=
   app (abs b) (new v).
-Obligation Tactic := idtac.
+Local Obligation Tactic := idtac.
 
 Equations in_app_weaken {Σ Σ' Σ'' : StoreTy} {t} (p : t ∈ (Σ ++ Σ'')) : t ∈ (Σ ++ Σ' ++ Σ'') by struct Σ :=
   in_app_weaken (Σ:=nil) p := pres_in (Σ', eq_refl) t p;
diff --git a/examples/definterp_scope.v b/examples/disabled/definterp_scope.v
similarity index 98%
rename from examples/definterp_scope.v
rename to examples/disabled/definterp_scope.v
index 107947aab..0a4ce294e 100644
--- a/examples/definterp_scope.v
+++ b/examples/disabled/definterp_scope.v
@@ -1,7 +1,7 @@
-Require Import Program.Basics Program.Tactics.
-From Equations.Prop Require Import Equations
-Require Import Stdlib.Vectors.VectorDef.
-Require Import List.
+From Stdlib Require Import Program.Basics Program.Tactics.
+From Equations.Prop Require Import Equations.
+From Stdlib Require Import Vectors.VectorDef.
+From Stdlib Require Import List.
 Import ListNotations.
 Set Equations Transparent.
 
@@ -171,7 +171,7 @@ Infix "⊚" := trans_incl (at level 10).
 Equations M : forall (Γ : Ctx) (P : StoreTy -> Type) (Σ : StoreTy), Type :=
   M Γ P Σ := forall (E : Env Γ Σ) (μ : Store Σ), option &{ Σ' : _ & &{ _ : Store Σ' & &{ _ : P Σ' & Σ ⊑ Σ'}}}.
 
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 Notation "( x , .. , y , z )" := (sigmaI _ x .. (sigmaI _ y z) ..) : core_scope.
 
 Equations bind {Σ Γ} {P Q : StoreTy -> Type} (f : M Γ P Σ) (g : ∀ {Σ'}, P Σ' -> M Γ Q Σ') : M Γ Q Σ :=
diff --git a/examples/definterp_simple.v b/examples/disabled/definterp_simple.v
similarity index 94%
rename from examples/definterp_simple.v
rename to examples/disabled/definterp_simple.v
index 0f859222f..53346d286 100644
--- a/examples/definterp_simple.v
+++ b/examples/disabled/definterp_simple.v
@@ -1,7 +1,8 @@
-Require Import Program.Basics Program.Tactics.
-From Equations.Prop Require Import Equations
+From Stdlib Require Import Program.Basics Program.Tactics.
+From Equations.Prop Require Import Equations.
+Set Warnings "-warn-library-file-stdlib-vector".
 Require Import Stdlib.Vectors.VectorDef.
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 Set Equations Transparent.
 
@@ -19,6 +20,7 @@ Definition Ctx := list Ty.
 
 Reserved Notation " x ∈ s " (at level 70, s at level 10).
 
+#[universes(template)]
 Inductive In {A} (x : A) : list A -> Type :=
 | here {xs} : x ∈ (x :: xs)
 | there {y xs} : x ∈ xs -> x ∈ (y :: xs)
@@ -69,7 +71,7 @@ Equations update : forall {A P xs} {x : A}, All P xs -> x ∈ xs -> P x -> All P
 Equations M : Ctx -> Type -> Type :=
   M Γ A := Env Γ -> option A.
 
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 
 Equations bind : ∀ {Γ A B}, M Γ A → (A → M Γ B) → M Γ B :=
   bind m f γ := match m γ with
diff --git a/examples/function_iter_style.v b/examples/disabled/function_iter_style.v
similarity index 96%
rename from examples/function_iter_style.v
rename to examples/disabled/function_iter_style.v
index 7f7b41a4a..e01b9f454 100644
--- a/examples/function_iter_style.v
+++ b/examples/disabled/function_iter_style.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List Program.Syntax Arith Lia.
+From Stdlib Require Import List Program.Syntax Arith Lia.
 
 Equations div2 (n : nat) : nat :=
   div2 0 := 0;
diff --git a/examples/misc.v b/examples/disabled/misc.v
similarity index 91%
rename from examples/misc.v
rename to examples/disabled/misc.v
index 1777caebb..30ac78564 100644
--- a/examples/misc.v
+++ b/examples/disabled/misc.v
@@ -1,5 +1,7 @@
+From Equations.Prop Require Import Equations.
+From Stdlib Require Import List.
 
-
+Import List_Notations.
 
 (** In general, one can require more elaborate loop invariants.
     This [fast_length] function computes the length of a list using
@@ -29,7 +31,7 @@ Equations list_init {A} (n : nat) (a : A) : list A :=
   list_init 0 _ := [];
   list_init (S n) x := x :: list_init n x.
 
-Require Import NArith.
+From Stdlib Require Import NArith.
 
 Equations pos_list_init {A} (n : positive) (a : A) : list A :=
   pos_list_init xH x := [x];
diff --git a/examples/nm.v b/examples/disabled/nm.v
similarity index 98%
rename from examples/nm.v
rename to examples/disabled/nm.v
index eb1b92612..c398a4e1d 100644
--- a/examples/nm.v
+++ b/examples/disabled/nm.v
@@ -1,7 +1,7 @@
 (** Proving Termination of Normalization Functions for Conditional Expressions, L. Paulson *)
 From Equations.Prop Require Import Equations.
 
-Require Import List Program.Syntax Arith Lia.
+From Stdlib Require Import List Program.Syntax Arith Lia.
 
 Inductive exp := At | If : exp -> exp -> exp -> exp.
 
diff --git a/examples/quicksort.v b/examples/disabled/quicksort.v
similarity index 96%
rename from examples/quicksort.v
rename to examples/disabled/quicksort.v
index ded0c0031..5cb0f1eb4 100644
--- a/examples/quicksort.v
+++ b/examples/disabled/quicksort.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Vector.
+From Stdlib Require Import Vector.
 Notation vector := t.
 Derive NoConfusion NoConfusionHom for vector.
 
@@ -44,13 +44,13 @@ Proof.
   firstorder.
 Qed.
 
-(* Lemma All_In_All {A P n m} (v : vector A n) (v' : vector A m) : *)
-(*   All (fun x => In x v) v' -> All P v -> All P v'. *)
-(* Proof. *)
-(*   induction 1. simpl. constructor. *)
-(*   intros. constructor; auto. *)
-(*   eapply In_All; eauto. *)
-(* Qed. *)
+Lemma All_In_All {A P n m} (v : vector A n) (v' : vector A m) :
+   All (fun x => In x v) v' -> All P v -> All P v'.
+Proof.
+  induction 1. simpl. constructor.
+  intros. constructor; auto.
+  eapply In_All; eauto.
+Qed.
 
 Inductive Sorted {A : Type} (R : A -> A -> Prop) : forall {n}, vector A n -> Prop :=
 | Sorted_nil : Sorted R nil
@@ -70,7 +70,7 @@ Proof.
   split; intros; depelim H0; cbn; simp In app in *; intuition eauto with *; simp In in *.
   apply H in H0. intuition.
 Qed.
-Require Import Sumbool.
+From Stdlib Require Import Sumbool.
 
 Notation dec x := (sumbool_of_bool x).
 
diff --git a/examples/dune b/examples/dune
new file mode 100644
index 000000000..45db7c6d9
--- /dev/null
+++ b/examples/dune
@@ -0,0 +1,10 @@
+(coq.theory
+ ; This determines the -R flag
+ (name Equations.Examples)
+ (package rocq-equations-examples)
+ (synopsis "Equations Plugin Examples")
+ (plugins rocq-runtime.plugins.extraction rocq-equations.plugin)
+ (modules :standard \ IdDec NoCycle)
+ (theories Stdlib Equations Equations.Prop Equations.Type))
+
+(include_subdirs no)
\ No newline at end of file
diff --git a/examples/general_recursion.v b/examples/general_recursion.v
index 0e438007a..34c285215 100644
--- a/examples/general_recursion.v
+++ b/examples/general_recursion.v
@@ -24,12 +24,13 @@
 (** printing NoConfusion %\coqdocclass{NoConfusion}% *)
 From Equations.Prop Require Import Equations.
 
-Require Import ZArith Lia.
-Require Import Program.
-Require Import Psatz.
-Require Import Nat.
-Require Import Stdlib.Vectors.VectorDef.
-Require Import Relations.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import Program.
+From Stdlib Require Import Psatz.
+From Stdlib Require Import Nat.
+#[warnings="-warn-library-file-stdlib-vector"]
+From Stdlib Require Import Vectors.VectorDef.
+From Stdlib Require Import Relations.
 
 Set Keyed Unification.
 Set Equations Transparent.
@@ -50,6 +51,8 @@ Instance wf_total_init_compute : forall {A}, WellFounded (@total_relation A).
   exact (fun A => Acc_intro_generator 10 wf_total_init).
 Defined.
 
+Set Warnings "-solve_obligation_error".
+
 (** Now we define an obviously non-terminating function. *)
 Equations? nonterm (n : nat) : nat by wf n (@total_relation nat) :=
   nonterm 0 := 0;
@@ -124,6 +127,7 @@ Definition fact :=
        | 0 => 1
        | S n => S n * fact n
        end).
+#[warnings="-abstract-large-number"]
 Check eq_refl : fact 8 = 40320.
 
 (** [Y] is only good in call-by-name or call-by-need, so we switch to Haskell *)
diff --git a/examples/graph_complete.v b/examples/graph_complete.v
index 272618611..ab912a17c 100644
--- a/examples/graph_complete.v
+++ b/examples/graph_complete.v
@@ -1,8 +1,9 @@
 Set Warnings "-notation-overridden".
 From Equations.Type Require Import All.
+#[warning="-notation-incompatible-prefix"]
 Require Import Examples.HoTT_light.
 Set Universe Polymorphism.
-Require Import Relations.
+From Stdlib Require Import Relations.
 
 Import Id_Notations.
 Import Sigma_Notations.
diff --git a/examples/mutualwfrec.v b/examples/mutualwfrec.v
index 643ee37ca..1f7e60a72 100644
--- a/examples/mutualwfrec.v
+++ b/examples/mutualwfrec.v
@@ -9,7 +9,7 @@
 
 From Equations.Prop Require Import Equations.
 From Stdlib Require Import List Syntax Arith Lia.
-Require Import List Wellfounded.
+From Stdlib Require Import List Wellfounded.
 Import ListNotations.
 (* end hide *)
 (** * Mutual well-founded recursion using dependent pattern-matching
diff --git a/examples/nested_mut_rec.v b/examples/nested_mut_rec.v
index e6eac18f4..d2b09d09a 100644
--- a/examples/nested_mut_rec.v
+++ b/examples/nested_mut_rec.v
@@ -6,7 +6,7 @@
 
 From Equations.Prop Require Import Equations.
 
-Require Import Program Arith List Compare_dec.
+From Stdlib Require Import Program Arith List Compare_dec.
 Import ListNotations.
 
 (** A nested recursive definition of terms with lists of terms *)
diff --git a/examples/ordinals.v b/examples/ordinals.v
index 177961172..d0ca2e363 100644
--- a/examples/ordinals.v
+++ b/examples/ordinals.v
@@ -1,8 +1,8 @@
-Require Import Arith.
+From Stdlib Require Import Arith.
 From Stdlib Require Import Eqdep_dec.
 From Stdlib Require Import Peano_dec.
-Require Import List.
-Require Import Recdef.
+From Stdlib Require Import List.
+From Stdlib Require Import Recdef.
 
 (**
   Arithmétique
@@ -150,7 +150,7 @@ Qed.
 Lemma padd_len_le_len : forall (w1 w2:(list nat)),
   (le (length w1) (length w2))
   -> (length (padd w1 w2)) = (length w2).
-intros. unfold padd. unfold dist. rewrite app_length.
+intros. unfold padd. unfold dist. rewrite length_app.
 rewrite zs_len.
 rewrite Nat.sub_add by (exact H); reflexivity.
 Qed.
@@ -551,7 +551,7 @@ Qed.
 (**
   Applications avec Program Fixpoint
 *)
-Require Coq.Program.Wf.
+From Stdlib Require Program.Wf.
 
 (* Tactique pour les preuves de bonne fondation. *)
 Ltac by_Acc_mwlt mwlt := 
diff --git a/examples/polynomials.v b/examples/polynomials.v
index 9010aa1b3..2b9f85561 100644
--- a/examples/polynomials.v
+++ b/examples/polynomials.v
@@ -17,12 +17,13 @@
   2016-2017. If running this interactively you can ignore the printing
   and hide directives which are just used to instruct coqdoc. *)
 (* begin hide *)
-Require Import Program.Basics Program.Tactics.
+From Stdlib Require Import Program.Basics Program.Tactics.
 From Equations.Prop Require Import Equations.
 
-Require Import ZArith Lia.
-Require Import Psatz.
-Require Import Nat.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import Psatz.
+From Stdlib Require Import Nat.
+#[warnings="-warn-library-file-stdlib-vector"]
 Require Import Stdlib.Vectors.VectorDef.
 
 Set Keyed Unification.
diff --git a/examples/string_matching.v b/examples/string_matching.v
index ed22a8d0e..509826c95 100644
--- a/examples/string_matching.v
+++ b/examples/string_matching.v
@@ -1,11 +1,11 @@
 (** Example by Nicky Vazou, unfinished *)
 
-Require Import Arith.
+From Stdlib Require Import Arith.
 From Stdlib Require Import DecidableClass.
 From Stdlib.Program Require Import Wf.
-Require Import List Lia.
-Require Import PeanoNat.
-Require Import Program.
+From Stdlib Require Import List Lia.
+From Stdlib Require Import PeanoNat.
+From Stdlib Require Import Program.
 From Equations.Prop Require Import Equations.
 
 Import ListNotations.
@@ -236,7 +236,7 @@ Section pmconcat.
     | left H => mconcat x ;
     | right Hd => pmconcat i (map mconcat (chunk i x)) }.
   Proof. clear pmconcat.
-    rewrite map_length.
+    rewrite length_map.
     rewrite Bool.orb_false_iff in Hd.
     destruct Hd. apply leb_complete_conv in H2. apply leb_complete_conv in H3.
     apply length_chunk_lt; simpl; auto.
diff --git a/examples/wfrec.v b/examples/wfrec.v
index 9b7b0bfa3..b4d6233b8 100644
--- a/examples/wfrec.v
+++ b/examples/wfrec.v
@@ -9,7 +9,7 @@
 
 From Equations.Prop Require Import Equations.
 From Stdlib Require Import List Syntax Arith Lia.
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 (* end hide *)
 (** * Well-founded recursion
diff --git a/src/equations.ml b/src/equations.ml
index b83c396ff..2a7397365 100644
--- a/src/equations.ml
+++ b/src/equations.ml
@@ -83,11 +83,11 @@ let define_unfolding_eq ~pm env evd flags p unfp prog prog' ei hook =
          (mkApp (funfc, extended_rel_vect 0 sign))) sign
   in
   let evd, stmt = Typing.solve_evars (Global.env ()) !evd stmt in
-  let subproofs = Principles_proofs.extract_subprograms env evd ei.equations_where_map p unfp in
+  let subproofs = Principles_proofs.extract_subprograms env evd ei.Principles_proofs.equations_where_map p unfp in
   let fold pm (name, subst, uctx, typ) =
     let typ = EConstr.Unsafe.to_constr typ in
     let typ = collapse_term_qualities uctx typ in
-    let tac = Principles_proofs.prove_unfolding_sublemma info ei.equations_where_map prog.program_cst funf_cst subst in
+    let tac = Principles_proofs.prove_unfolding_sublemma info ei.Principles_proofs.equations_where_map prog.program_cst funf_cst subst in
     let cinfo = Declare.CInfo.make ~name ~typ () in
     let info = Declare.Info.make ~poly:info.poly
         ~scope:info.scope
diff --git a/src/equations_common.ml b/src/equations_common.ml
index 9b8aa8982..1649e4139 100644
--- a/src/equations_common.ml
+++ b/src/equations_common.ml
@@ -45,7 +45,7 @@ let equations_category = CWarnings.create_category ~name:"equations" ()
 
 let () = Goptions.declare_bool_option {
   Goptions.optdepr  = Some depr_with_k;
-  Goptions.optstage = Interp;
+  Goptions.optstage = Summary.Stage.Interp;
   Goptions.optkey   = ["Equations"; "WithK"];
   Goptions.optread  = (fun () -> false);
   Goptions.optwrite = (fun b ->
@@ -58,7 +58,7 @@ let () = Goptions.declare_bool_option {
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = Some depr_with_k;
-  Goptions.optstage = Interp;
+  Goptions.optstage = Summary.Stage.Interp;
   Goptions.optkey   = ["Equations"; "WithKDec"];
   Goptions.optread  = (fun () -> !simplify_withUIP);
   Goptions.optwrite = (fun b -> simplify_withUIP := b)
@@ -66,7 +66,7 @@ let _ = Goptions.declare_bool_option {
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = None;
-  Goptions.optstage = Interp;
+  Goptions.optstage = Summary.Stage.Interp;
   Goptions.optkey   = ["Equations"; "With"; "UIP"];
   Goptions.optread  = (fun () -> !simplify_withUIP);
   Goptions.optwrite = (fun b -> simplify_withUIP := b)
@@ -74,7 +74,7 @@ let _ = Goptions.declare_bool_option {
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = None;
-  Goptions.optstage = Interp;
+  Goptions.optstage = Summary.Stage.Interp;
   Goptions.optkey   = ["Equations"; "Transparent"];
   Goptions.optread  = (fun () -> !equations_transparent);
   Goptions.optwrite = (fun b -> equations_transparent := b)
@@ -82,7 +82,7 @@ let _ = Goptions.declare_bool_option {
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = None;
-  Goptions.optstage = Interp;
+  Goptions.optstage = Summary.Stage.Interp;
   Goptions.optkey   = ["Equations"; "With"; "Funext"];
   Goptions.optread  = (fun () -> !equations_with_funext);
   Goptions.optwrite = (fun b -> equations_with_funext := b)
@@ -90,7 +90,7 @@ let _ = Goptions.declare_bool_option {
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = None;
-  Goptions.optstage = Interp;
+  Goptions.optstage = Summary.Stage.Interp;
   Goptions.optkey   = ["Equations"; "Derive"; "Equations"];
   Goptions.optread  = (fun () -> !equations_derive_equations);
   Goptions.optwrite = (fun b -> equations_derive_equations := b)
@@ -98,7 +98,7 @@ let _ = Goptions.declare_bool_option {
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = None;
-  Goptions.optstage = Interp;
+  Goptions.optstage = Summary.Stage.Interp;
   Goptions.optkey   = ["Equations"; "Derive"; "Eliminator"];
   Goptions.optread  = (fun () -> !equations_derive_eliminator);
   Goptions.optwrite = (fun b -> equations_derive_eliminator := b)
@@ -110,7 +110,7 @@ let debug = ref false
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = None;
-  Goptions.optstage = Interp;
+  Goptions.optstage = Summary.Stage.Interp;
   Goptions.optkey   = ["Equations"; "Debug"];
   Goptions.optread  = (fun () -> !debug);
   Goptions.optwrite = (fun b -> debug := b)
@@ -222,6 +222,7 @@ let e_type_of env evd t =
   evd := evm; t
 
 let collapse_term_qualities uctx c =
+  let open Sorts.Quality in
   let nf_qvar q = match UState.nf_qvar uctx q with
     | QConstant _ as q -> q
     | QVar q -> (* hack *) QConstant QType
@@ -1091,7 +1092,7 @@ let evd_comb1 f evd x =
 (* Universe related functions *)
 
 [%%if rocq = "9.1"]
-let set_leq_sort _ = Evd.set_leq_sort
+let set_leq_sort _env = Evd.set_leq_sort
 [%%else]
 let set_leq_sort env = Evd.set_leq_sort env
 [%%endif]
@@ -1110,7 +1111,7 @@ let nonalgebraic_universe_level_of_universe env sigma u =
     | None ->
       let sigma, l = Evd.new_univ_level_variable Evd.univ_flexible sigma in
       let ul = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make l in
-      let sigma = Evd.set_leq_sort env sigma u ul in
+      let sigma = set_leq_sort env sigma u ul in
       sigma, l, ul
 
 let instance_of env sigma ?argu goalu =
diff --git a/src/principles_proofs.ml b/src/principles_proofs.ml
index 8bdf1c906..7dd2996b4 100644
--- a/src/principles_proofs.ml
+++ b/src/principles_proofs.ml
@@ -210,7 +210,7 @@ let mutual_fix li l =
 let check_guard gls env sigma =
   let gl = Proofview.drop_state (List.hd gls) in
   try
-    let EvarInfo evi = Evd.find sigma gl in
+    let Evd.EvarInfo evi = Evd.find sigma gl in
     match Evd.evar_body evi with
     | Evd.Evar_defined b -> Inductiveops.control_only_guard (Evd.evar_env env evi) sigma b; true
     | Evd.Evar_empty -> true
diff --git a/src/simplify.ml b/src/simplify.ml
index 683cbf098..f4471869d 100644
--- a/src/simplify.ml
+++ b/src/simplify.ml
@@ -418,7 +418,7 @@ let compose_term (env : Environ.env) (evd : Evd.evar_map ref)
   ((h1, c1) : open_term) ((h2, c2) : open_term) : open_term =
   match h1 with
   | Some ((ctx1, _, u1), (ev1, _)) ->
-      let EvarInfo ev1_info = Evd.find !evd ev1 in
+      let Evd.EvarInfo ev1_info = Evd.find !evd ev1 in
       let ev1_ctx = Evd.evar_context ev1_info in
       (* Keep only the context corresponding to [ctx1]. *)
       let named_ctx1 = CList.firstn (List.length ctx1) ev1_ctx in
@@ -795,7 +795,7 @@ SimpFun.make ~name:"solution" begin fun (env : Environ.env) (evd : Evd.evar_map
           checked_appvect env evd tsolution [| tA'; term'; tB'; c; trel' |]
       in
       (* We make some room for the application of the equality... *)
-      let env = push_rel (LocalAssum (name, ty1')) env in
+      let env = push_rel (Context.Rel.Declaration.LocalAssum (name, ty1')) env in
       let c = Vars.lift 1 c in
       let c = checked_appvect env evd c [| EConstr.mkRel 1 |] in
       (* [targs'] are arguments in the context [eq_decl :: ctx']. *)
diff --git a/src/splitting.ml b/src/splitting.ml
index 560b7ec3b..d035f4a0f 100644
--- a/src/splitting.ml
+++ b/src/splitting.ml
@@ -1112,8 +1112,9 @@ let gather_fresh_context sigma u octx =
   let qarr, uarr = UVars.Instance.to_array u in
   let qualities =
     Array.fold_left (fun ctx' l ->
+        let open Sorts.Quality in
         match l with
-        | Sorts.Quality.QConstant _ -> assert false
+        | QConstant _ -> assert false
         | QVar l ->
           if not (Sorts.QVar.Set.mem l qvars) then Sorts.QVar.Set.add l ctx'
           else ctx')
diff --git a/test-suite/Basics.v b/test-suite/Basics.v
index cc2f76bdd..5cc482348 100644
--- a/test-suite/Basics.v
+++ b/test-suite/Basics.v
@@ -6,10 +6,10 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-Require Import Program Bvector List Relations.
+From Stdlib Require Import Program List Relations.
 From Equations.Prop Require Import Equations.
 
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 Set Keyed Unification.
 
 Equations neg (b : bool) : bool :=
@@ -105,7 +105,7 @@ Derive Signature for vector.
 Derive NoConfusion NoConfusionHom for vector.
 Derive Subterm for vector.
 
-Require Import Arith Wf_nat.
+From Stdlib Require Import Arith Wf_nat.
 
 #[local]
 Instance wf_nat : WellFounded lt := lt_wf.
@@ -122,7 +122,8 @@ testn (S n) with testn n => {
   | 0 := S 0 ;
   | (S n') := S n' }.
 
-Require Import Vectors.Vector.
+#[warnings="-warn-library-file-stdlib-vector"]  
+From Stdlib Require Import Vectors.Vector.
 
 Arguments Vector.nil {A}.
 Arguments Vector.cons {A} _ {n}.
@@ -436,8 +437,6 @@ Extraction split. *)
 
 (* Eval compute in @zip''. *)
 
-Require Import Bvector.
-
 Equations  split_struct {X : Type} {m n} (xs : vector X (m + n)) : Split m n xs :=
 split_struct (m:=0) xs := append nil xs ;
 split_struct (m:=(S m)) (cons x xs) with split_struct xs => {
@@ -623,13 +622,14 @@ Definition transpose {A m n} : mat A m n -> mat A n m :=
 (*   (e : vector (vector A 0) n) v : vfold_right f (vmake n Vnil) v =  *)
 (* Typeclasses eauto :=. *)
 
-Require Import fin.
+From Equations.TestSuite Require Import fin.
 
 Generalizable All Variables.
 
 Opaque vmap. Opaque vtail. Opaque nth.
 
-Require Vectors.Vector.
+#[warnings="-warn-library-file-stdlib-vector"]
+From Stdlib Require Vectors.Vector.
 Arguments Vector.nil {A}.
 Arguments Vector.cons {A} _ {n}.
 Notation vnil := Vector.nil.
diff --git a/test-suite/BasicsDec.v b/test-suite/BasicsDec.v
index bf335060a..0718fca7b 100644
--- a/test-suite/BasicsDec.v
+++ b/test-suite/BasicsDec.v
@@ -1,4 +1,5 @@
 From Equations.Prop Require Import Equations.
+#[warnings="-deprecated-library-file-since-8.20"]
 From Stdlib Require Import Bvector.
   
 Inductive bar1 (A : Type) : A -> Prop := .
diff --git a/test-suite/Below.v b/test-suite/Below.v
index 29f756d56..2c6314e18 100644
--- a/test-suite/Below.v
+++ b/test-suite/Below.v
@@ -10,6 +10,7 @@
    [equations] when it needs to do recursion on a type. *)
 
 Set Warnings "-deprecated-library-file-since-8.20".
+Set Warnings "-warn-library-file-stdlib-vector".
 From Stdlib Require Import Bvector Vectors.Vector.
 From Equations Require Import Init CoreTactics.
 From Equations.Prop Require Import DepElim Tactics Constants FunctionalInduction.
diff --git a/test-suite/DataStruct.v b/test-suite/DataStruct.v
index d8aa99442..623f55add 100644
--- a/test-suite/DataStruct.v
+++ b/test-suite/DataStruct.v
@@ -1,7 +1,7 @@
 (* http://adam.chlipala.net/cpdt/html/DataStruct.html *)
 
-Require Import Arith List.
-Require Import Program Equations.Prop.Equations.
+From Stdlib Require Import Arith List Program.
+From Equations.Prop Require Import Equations.
 Set Implicit Arguments.
 Set Keyed Unification.
 
diff --git a/test-suite/HoTT/BasicsHoTT.v b/test-suite/HoTT/BasicsHoTT.v
index d922b6d4b..fbc592659 100644
--- a/test-suite/HoTT/BasicsHoTT.v
+++ b/test-suite/HoTT/BasicsHoTT.v
@@ -6,10 +6,10 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 From Equations Require Import CoreTactics.
-Require Import Equations.HoTT.All Equations.HoTT.WellFounded.
+From Equations Require Import HoTT.All Equations.HoTT.WellFounded.
 Require Import Stdlib.Unicode.Utf8.
 Require HoTT.Basics.Overture.
-Require Import HoTT.Types.Bool HoTT.Spaces.Nat HoTT.Spaces.List.Core.
+From Stdlib Require Import HoTT.Types.Bool HoTT.Spaces.Nat HoTT.Spaces.List.Core.
 
 Local Open Scope nat_scope.
 
@@ -124,7 +124,7 @@ testn (S n) with testn n => {
 Local Open Scope vect_scope.
 Reserved Notation "x ++v y" (at level 60).
 
-Require Import HoTT.Classes.implementations.peano_naturals.
+From Stdlib Require Import HoTT.Classes.implementations.peano_naturals.
 (* Require Import HoTT.Classes.interfaces.canonical_names. *)
 
 Equations vapp {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m)%nat :=
@@ -137,7 +137,7 @@ where "x ++v y" := (vapp x y).
 Set Universe Minimization ToSet.
 Derive NoConfusionHom for vector.
 Unset Universe Minimization ToSet.
-Require Import Equations.HoTT.Tactics.
+From Equations Require Import HoTT.Tactics.
 
 #[local] Instance vector_eqdec@{i +|+} {A : Type@{i}} {n} `(EqDec@{i} A) : EqDec (vector A n).
 Proof.
diff --git a/test-suite/LogicType.v b/test-suite/LogicType.v
index 6c1d14816..bd0d93050 100644
--- a/test-suite/LogicType.v
+++ b/test-suite/LogicType.v
@@ -35,9 +35,8 @@ Arguments vector A%_type_scope n%_nat_scope.
 Arguments nil {A}.
 Arguments cons {A%_type_scope} {n%_nat_scope} a v.
 Derive Signature for vector.
-Require Import Equations.CoreTactics Equations.Type.Tactics.
-From Equations.Type Require Import Tactics.
-From Equations.Type Require Import FunctionalInduction.
+From Equations Require Import CoreTactics.
+From Equations.Type Require Import Tactics FunctionalInduction.
 
 Set Universe Minimization ToSet.
 Derive NoConfusionHom for vector.
diff --git a/test-suite/ack.v b/test-suite/ack.v
index ddfcf99bf..beb35be14 100644
--- a/test-suite/ack.v
+++ b/test-suite/ack.v
@@ -1,5 +1,5 @@
 (* https://lawrencecpaulson.github.io/2022/08/31/Ackermann-not-PR-I.html *)
-Require Import Arith Lia.
+From Stdlib Require Import Arith Lia.
 From Equations.Prop Require Import Equations.
 
 Equations ack (p : nat * nat) : nat by wf p (lexprod _ _ lt lt) :=
diff --git a/test-suite/agda_1408.v b/test-suite/agda_1408.v
index b96845c7c..3ed03a9e3 100644
--- a/test-suite/agda_1408.v
+++ b/test-suite/agda_1408.v
@@ -17,5 +17,6 @@ Inductive P : forall {i}, D i -> Set :=
 Derive Signature for P.
 Derive NoConfusionHom for P.
 
+#[warning="-solve_obligation_error,functional-induction-derivation-failure"]
 Equations Foo (p : P d1) : Set :=
   Foo p1 := nat.
diff --git a/test-suite/agda_1775.v b/test-suite/agda_1775.v
index 0ee3dc83d..4e6dae7bb 100644
--- a/test-suite/agda_1775.v
+++ b/test-suite/agda_1775.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 (* Set Universe Polymorphism. *)
 (** Can we define NoConfusion in SProp (squashing equalities of arguments)?
     Would not allow to show equivalence to (x = y) for non-strict sets. *)
diff --git a/test-suite/cfold.v b/test-suite/cfold.v
index 30e157ca9..6214b311d 100644
--- a/test-suite/cfold.v
+++ b/test-suite/cfold.v
@@ -2,10 +2,10 @@
    Proof size is now constant instead of quadratic.,
    but program is as straightforward as in Agda. *)
 
-Require Import Arith.
+From Stdlib Require Import Arith.
 From Equations.Prop Require Import Equations.
 
-Require Import Stdlib.Bool.Bool.
+From Stdlib Require Import Bool.Bool.
 
 Set Keyed Unification.
 Set Implicit Arguments.
diff --git a/test-suite/disabled/agda_1775_full.v b/test-suite/disabled/agda_1775_full.v
index c4be549bb..4eedce685 100644
--- a/test-suite/disabled/agda_1775_full.v
+++ b/test-suite/disabled/agda_1775_full.v
@@ -40,7 +40,7 @@ Definition equiv_adj {A B} {E: Equiv A B} (x : A)
 
 Notation " 'rew' H 'in' c " := (@eq_rect _ _ _ c _ H) (at level 20).
 
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 
 Notation " X <~> Y " := (Equiv X Y) (at level 90, no associativity, Y at next level).
 
diff --git a/test-suite/disabled/noconf_hom.v b/test-suite/disabled/noconf_hom.v
index caf6b1ea0..b54440a4e 100644
--- a/test-suite/disabled/noconf_hom.v
+++ b/test-suite/disabled/noconf_hom.v
@@ -1,7 +1,7 @@
 Set Warnings "-deprecated-library-file-since-8.20".
 From Stdlib Require Import Program Bvector List Relations.
 From Equations Require Import Equations Signature.
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 Unset Equations WithK.
 
 Inductive Vec (A : Set) : nat -> Set :=
diff --git a/test-suite/disabled/scope_noK.v b/test-suite/disabled/scope_noK.v
index 81d919896..0ec673809 100644
--- a/test-suite/disabled/scope_noK.v
+++ b/test-suite/disabled/scope_noK.v
@@ -1,12 +1,11 @@
 (** Example by Rafaël Bocquet: POPLmark part 1A with inductive definition of scope 
   and well-scoped variables (and terms, types and environments). *)
 
-From Equations.Prop Require Import Equations
-
+From Equations.Prop Require Import Equations.
 Require Import Stdlib.Logic.Eqdep_dec.
 Require Import Stdlib.Classes.EquivDec.
-Require Import Program.
-Require Import Arith.
+From Stdlib Require Import Program.
+From Stdlib Require Import Arith.
 
 Ltac simpl_exist :=
   repeat (
diff --git a/test-suite/f91.v b/test-suite/f91.v
index c06ea6d41..a24658ae3 100644
--- a/test-suite/f91.v
+++ b/test-suite/f91.v
@@ -6,7 +6,7 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-From Stdlib Require Import Program Bvector List Relations Lia Arith Wf_nat.
+From Stdlib Require Import Program List Relations Lia Arith Wf_nat.
 From Equations.Prop Require Import Equations.
 
 Set Program Mode.
diff --git a/test-suite/fin.v b/test-suite/fin.v
index 14926e622..97b321806 100644
--- a/test-suite/fin.v
+++ b/test-suite/fin.v
@@ -1,4 +1,5 @@
-Require Import Program Equations.Prop.EqDecInstances Equations.Prop.Equations.
+From Stdlib Require Import Program.
+From Equations.Prop Require Import EqDecInstances Equations.
 Import Sigma_Notations.
 Local Open Scope equations_scope.
 Set Equations Transparent.
diff --git a/test-suite/fle_trans.v b/test-suite/fle_trans.v
index 34dd64284..af827a6fa 100644
--- a/test-suite/fle_trans.v
+++ b/test-suite/fle_trans.v
@@ -51,7 +51,7 @@ Print Assumptions fle_trans.
   %\texttt{Closed under the global context}%
 *)
 (* end hide *)
-Require Import Program.
+From Stdlib Require Import Program.
 (* begin hide *)
 Fixpoint fle_trans' {n : nat} {i j k : fin n}
   (p : fle i j) (q : fle j k) : fle i k.
diff --git a/test-suite/gcd.v b/test-suite/gcd.v
index a93d64e9f..4810e3001 100644
--- a/test-suite/gcd.v
+++ b/test-suite/gcd.v
@@ -1,7 +1,7 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Relations.
-Require Import Arith Lia.
+From Stdlib Require Import Relations.
+From Stdlib Require Import Arith Lia.
 Set Keyed Unification.
 
 Ltac subst_lets :=
@@ -25,7 +25,7 @@ gcd x y with gt_eq_gt_dec x y := {
 Transparent gcd.
 Eval compute in gcd 18 84.
 
-Require Import ExtrOcamlBasic.
+From Stdlib Require Import ExtrOcamlBasic.
 Extraction Inline pr1 pr2.
 Extraction gcd.
 (* Extraction gcd_unfold. *)
diff --git a/test-suite/innacs.v b/test-suite/innacs.v
index 505001ca5..76a5a5551 100644
--- a/test-suite/innacs.v
+++ b/test-suite/innacs.v
@@ -1,7 +1,8 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Vector.
-Require Import fin.
+#[warnings="-warn-library-file-stdlib-vector"]
+From Stdlib Require Import Vector.
+From Equations.TestSuite Require Import fin.
 Notation vector := Vector.t.
 Arguments Vector.nil {A}.
 Arguments Vector.cons {A} _ {n}.
diff --git a/test-suite/interval.v b/test-suite/interval.v
index 465744409..98bbf4dd2 100644
--- a/test-suite/interval.v
+++ b/test-suite/interval.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List Arith Lia.
+From Stdlib Require Import List Arith Lia.
 Import ListNotations.
 
 Set Keyed Unification.
diff --git a/test-suite/issues/coq_pr_16995.v b/test-suite/issues/coq_pr_16995.v
index 69e5f9b78..b8d300d32 100644
--- a/test-suite/issues/coq_pr_16995.v
+++ b/test-suite/issues/coq_pr_16995.v
@@ -27,7 +27,7 @@ Register Classes.NoConfusionPackage as equations.noconfusion.class.
 Register Classes.apply_noConfusion as equations.depelim.apply_noConfusion.
 Register DepElim.simplification_sigma1_dep as equations.depelim.simpl_sigma_dep.
 Register DepElim.opaque_ind_pack_inv as equations.depelim.opaque_ind_pack_eq_inv.
-Import Equations.CoreTactics.
+Import CoreTactics.
 
 Set Warnings "-notation-overridden".
 Import Equations.Type.Logic.
diff --git a/test-suite/issues/issue104.v b/test-suite/issues/issue104.v
index b315844a9..35b1baa55 100644
--- a/test-suite/issues/issue104.v
+++ b/test-suite/issues/issue104.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 (* This type is from VST:
  * https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L13 *)
 Fixpoint compact_sum (T: list Type): Type :=
diff --git a/test-suite/issues/issue105.v b/test-suite/issues/issue105.v
index b674a0ade..4f0147f9c 100644
--- a/test-suite/issues/issue105.v
+++ b/test-suite/issues/issue105.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 (* This type is from VST: 
  * https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L13 *)
 Fixpoint compact_sum (T: list Type): Type :=
diff --git a/test-suite/issues/issue107.v b/test-suite/issues/issue107.v
index 82cc8b0d1..d4f290b49 100644
--- a/test-suite/issues/issue107.v
+++ b/test-suite/issues/issue107.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 
 (* The rest is a nonsensical, just to give a minimalistic reproducible example *)
 Inductive Foo :=
diff --git a/test-suite/issues/issue107_2.v b/test-suite/issues/issue107_2.v
index c9ee7b672..67501907f 100644
--- a/test-suite/issues/issue107_2.v
+++ b/test-suite/issues/issue107_2.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 
 (* The rest is a nonsensical, just to give a minimalistic reproducible example *)
 Inductive Foo :=
diff --git a/test-suite/issues/issue124.v b/test-suite/issues/issue124.v
index 595fef982..077d9aea9 100644
--- a/test-suite/issues/issue124.v
+++ b/test-suite/issues/issue124.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 Equations foo (f: option (nat -> nat)) (l: list nat) : list nat :=
diff --git a/test-suite/issues/issue143.v b/test-suite/issues/issue143.v
index 9cedfc0fb..9c233cf60 100644
--- a/test-suite/issues/issue143.v
+++ b/test-suite/issues/issue143.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 Section Tests.
 
diff --git a/test-suite/issues/issue193.v b/test-suite/issues/issue193.v
index 8c0e0dc67..6f1628da0 100644
--- a/test-suite/issues/issue193.v
+++ b/test-suite/issues/issue193.v
@@ -1,4 +1,4 @@
-Require Import Program.
+From Stdlib Require Import Program.
 From Equations.Prop Require Import Equations.
 #[local]
 Obligation Tactic := program_simpl.
diff --git a/test-suite/issues/issue200.v b/test-suite/issues/issue200.v
index 76776bcde..ef1c6c98d 100644
--- a/test-suite/issues/issue200.v
+++ b/test-suite/issues/issue200.v
@@ -1,5 +1,5 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Vector.
+From Stdlib Require Import Vector.
 
 Derive DependentElimination for t.
diff --git a/test-suite/issues/issue212.v b/test-suite/issues/issue212.v
index 8ff4544d1..c43c09006 100644
--- a/test-suite/issues/issue212.v
+++ b/test-suite/issues/issue212.v
@@ -1,4 +1,4 @@
-Require Import List.
+From Stdlib Require Import List.
 From Stdlib Require Import Lia ssreflect.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
diff --git a/test-suite/issues/issue228.v b/test-suite/issues/issue228.v
index c09a4cf7f..3b15f1d39 100644
--- a/test-suite/issues/issue228.v
+++ b/test-suite/issues/issue228.v
@@ -1,7 +1,7 @@
-From Coq Require Import Utf8.
-From Coq Require Import Equality.
-From Coq Require Import Arith.
-From Coq Require Vector.
+From Stdlib Require Import Utf8.
+From Stdlib Require Import Equality.
+From Stdlib Require Import Arith.
+From Stdlib Require Vector.
 Import Vector.VectorNotations.
 From Equations.Prop Require Import Equations.
 
diff --git a/test-suite/issues/issue240.v b/test-suite/issues/issue240.v
index 56b00f2f0..8b9fd2b33 100644
--- a/test-suite/issues/issue240.v
+++ b/test-suite/issues/issue240.v
@@ -1,5 +1,4 @@
-From Equations.Prop Require Import Equations
-
+From Equations.Prop Require Import Equations.
 Inductive T1: Type :=
 | C { T: Type }: T1
 .
diff --git a/test-suite/issues/issue252.v b/test-suite/issues/issue252.v
index 2aa0f831b..19c5dcea5 100644
--- a/test-suite/issues/issue252.v
+++ b/test-suite/issues/issue252.v
@@ -1,5 +1,4 @@
-From Equations.Prop Require Import Equations
-
+From Equations.Prop Require Import Equations.
 Inductive vec (A:Type) : nat -> Type :=
   | nil : vec A 0
   | cons : forall n, A -> vec A n -> vec A (S n).
diff --git a/test-suite/issues/issue273.v b/test-suite/issues/issue273.v
index 502ce3433..e99efcec0 100644
--- a/test-suite/issues/issue273.v
+++ b/test-suite/issues/issue273.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 Inductive T := C : list T -> T.
 Show Obligation Tactic.
diff --git a/test-suite/issues/issue329.v b/test-suite/issues/issue329.v
index 0d422b453..993a1175e 100644
--- a/test-suite/issues/issue329.v
+++ b/test-suite/issues/issue329.v
@@ -1,4 +1,4 @@
-Require Import List ssreflect.
+From Stdlib Require Import List ssreflect.
 From Equations.Prop Require Import Equations.
 
 Import ListNotations.
diff --git a/test-suite/issues/issue349.v b/test-suite/issues/issue349.v
index e04db4520..15b971241 100644
--- a/test-suite/issues/issue349.v
+++ b/test-suite/issues/issue349.v
@@ -212,7 +212,7 @@ Program Lemma finite_subtree_domain_length_lt :
 Proof.
   unfold finite_subtree_domain, finite_subtree_domain'.
   intros (((? & ? & ? & ? & ?) & ?) & ?) ? ?.
-  rewrite map_length.
+  rewrite length_map.
   apply filter_length_lt'.
   induction π.
   - intuition.
diff --git a/test-suite/issues/issue389.v b/test-suite/issues/issue389.v
index 9a954a4a4..839c0b742 100644
--- a/test-suite/issues/issue389.v
+++ b/test-suite/issues/issue389.v
@@ -1,4 +1,4 @@
-Require Import Equations.HoTT.All.
+From Equations Require Import HoTT.All.
 Set Universe Polymorphism.
 Inductive A : Type :=
 | foo : A
diff --git a/test-suite/issues/issue393.v b/test-suite/issues/issue393.v
index bacd6116e..c4033dd71 100644
--- a/test-suite/issues/issue393.v
+++ b/test-suite/issues/issue393.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 
 Inductive In {X} (x : X) : list X -> Type :=
 | here {xs} : In x (x :: xs)
diff --git a/test-suite/issues/issue43.v b/test-suite/issues/issue43.v
index 832e6d33a..832aaaa11 100644
--- a/test-suite/issues/issue43.v
+++ b/test-suite/issues/issue43.v
@@ -1,5 +1,5 @@
-Require Import Program Bvector List.
-Require Import Relations.
+From Stdlib Require Import Program Bvector List.
+From Stdlib Require Import Relations.
 From Equations Require Import Equations DepElimDec.
 
 Equations silly {A} (l : list A) : list A :=
diff --git a/test-suite/issues/issue63.v b/test-suite/issues/issue63.v
index d9e61e74f..4aca5d212 100644
--- a/test-suite/issues/issue63.v
+++ b/test-suite/issues/issue63.v
@@ -1,6 +1,6 @@
 Require Import Stdlib.Vectors.Vector.
 Require Import Stdlib.PArith.PArith.
-Require Import Lia.
+From Stdlib Require Import Lia.
 From Equations.Prop Require Import Equations.
 
 Set Equations With UIP.
@@ -25,7 +25,7 @@ Arguments Ident {a tys dom}.
 Arguments Morph {a tys} f.
 Arguments Comp {a tys dom mid cod} f g.
 Import Sigma_Notations.
-Require Import Wellfounded Relations.
+From Stdlib Require Import Wellfounded Relations.
 
 Derive NoConfusion for positive.
 Derive EqDec for positive.
diff --git a/test-suite/issues/issue7.v b/test-suite/issues/issue7.v
index 0bd9ab86c..5f5157d50 100644
--- a/test-suite/issues/issue7.v
+++ b/test-suite/issues/issue7.v
@@ -1,6 +1,6 @@
 Set Warnings "-notation-overridden".
-Require Import ssreflect.
-Require Import Utf8 Program.
+From Stdlib Require Import ssreflect.
+From Stdlib Require Import Utf8 Program.
 From Equations.Prop Require Import Equations.
 
 
diff --git a/test-suite/issues/issue7_extr.v b/test-suite/issues/issue7_extr.v
index bcd5a5e1c..011538c6a 100644
--- a/test-suite/issues/issue7_extr.v
+++ b/test-suite/issues/issue7_extr.v
@@ -1,6 +1,6 @@
-Require Import Equations.Equations Utf8.
+From Equations Require Import Equations Utf8.
 Add Rec LoadPath ".." as Top.
-Require Import issue7.
+From Stdlib Require Import issue7.
 
 
 Extraction Inline apply_noConfusion.
diff --git a/test-suite/issues/issue8.v b/test-suite/issues/issue8.v
index 620d98f6c..12d86bf6b 100644
--- a/test-suite/issues/issue8.v
+++ b/test-suite/issues/issue8.v
@@ -1,4 +1,4 @@
-Require Import Utf8 Program.
+From Stdlib Require Import Utf8 Program.
 From Equations.Prop Require Import Equations.
 
 Open Scope equations_scope.
diff --git a/test-suite/issues/issue81.v b/test-suite/issues/issue81.v
index b77256da9..de0eeaf31 100644
--- a/test-suite/issues/issue81.v
+++ b/test-suite/issues/issue81.v
@@ -1,4 +1,4 @@
-Require Import Stdlib.Lists.List.
+From Stdlib Require Import Lists.List.
 Import ListNotations.
 From Equations.Prop Require Import Equations.
 
diff --git a/test-suite/issues/issue95_2.v b/test-suite/issues/issue95_2.v
index 3d160745c..efe962792 100644
--- a/test-suite/issues/issue95_2.v
+++ b/test-suite/issues/issue95_2.v
@@ -1,5 +1,5 @@
-Require Import TestSuite.issues.issue95_1.
-Require Import Lia.
+From Stdlib Require Import TestSuite.issues.issue95_1.
+From Stdlib Require Import Lia.
 From Equations.Prop Require Import Equations.
 
 
diff --git a/test-suite/local_where.v b/test-suite/local_where.v
index 11f349aee..f4519632e 100644
--- a/test-suite/local_where.v
+++ b/test-suite/local_where.v
@@ -1,4 +1,4 @@
-Require Import Program.Basics Program.Tactics.
+From Stdlib Require Import Program.Basics Program.Tactics.
 From Equations.Prop Require Import Equations.
 
 
diff --git a/test-suite/nestedobls.v b/test-suite/nestedobls.v
index 478424dc4..38abd3a41 100644
--- a/test-suite/nestedobls.v
+++ b/test-suite/nestedobls.v
@@ -9,14 +9,14 @@
 Set Asymmetric Patterns.
 Set Implicit Arguments.
 Unset Strict Implicit.
-Require Import Arith.
-Require Import Lia.
+From Stdlib Require Import Arith.
+From Stdlib Require Import Lia.
 From Equations.Prop Require Import Equations.
 
-Require Import Wellfounded Relation_Definitions.
-Require Import Relation_Operators Lexicographic_Product Wf_nat.
+From Stdlib Require Import Wellfounded Relation_Definitions.
+From Stdlib Require Import Relation_Operators Lexicographic_Product Wf_nat.
 Unset Implicit Arguments.
-Require Import Program.
+From Stdlib Require Import Program.
 
 Equations? test (n : nat) (pre : n >= 0 ) : { n' : nat | n' <= n }
  by wf n lt :=
diff --git a/test-suite/nestedrec2.v b/test-suite/nestedrec2.v
index 3155f086a..eb0e02cc7 100644
--- a/test-suite/nestedrec2.v
+++ b/test-suite/nestedrec2.v
@@ -1,7 +1,7 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Arith.
-Require Import Compare_dec.
+From Stdlib Require Import Arith.
+From Stdlib Require Import Compare_dec.
 
 Inductive term : Set :=
 | Var (n : nat)
diff --git a/test-suite/nestedwfrec.v b/test-suite/nestedwfrec.v
index eab2927be..3e79f1f8b 100644
--- a/test-suite/nestedwfrec.v
+++ b/test-suite/nestedwfrec.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 Equations? f (n : nat) : nat by wf n lt :=
   f 0 := 0;
diff --git a/test-suite/nestedwhererecwith.v b/test-suite/nestedwhererecwith.v
index deb004580..8d59d749f 100644
--- a/test-suite/nestedwhererecwith.v
+++ b/test-suite/nestedwhererecwith.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 Equations test {A} (n : nat) (gs : list A) : unit by wf n lt :=
diff --git a/test-suite/nestfixnorec.v b/test-suite/nestfixnorec.v
index 5ae91add2..311e0fa20 100644
--- a/test-suite/nestfixnorec.v
+++ b/test-suite/nestfixnorec.v
@@ -143,7 +143,7 @@ Section RoseTreeInd.
   list_tree_elim (cons a t) := fcons a t (tree_elim a) (list_tree_elim t) }.
 End RoseTreeInd.
 
-Require Import Bool.
+From Stdlib Require Import Bool.
 
 Module IdealNoSec.
 
diff --git a/test-suite/noconf_simplify.v b/test-suite/noconf_simplify.v
index dd365c4cf..052142b35 100644
--- a/test-suite/noconf_simplify.v
+++ b/test-suite/noconf_simplify.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 Record decl := { na : nat; body : option nat }.
diff --git a/test-suite/nocycle.v b/test-suite/nocycle.v
index 04d081411..458d1b59e 100644
--- a/test-suite/nocycle.v
+++ b/test-suite/nocycle.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Below.
+From Equations.TestSuite Require Import Below.
 Module NoCycle_nat.
 
 Definition noSubterm x y :=
@@ -293,7 +293,7 @@ Module NoCycle_mut.
   Qed.
 End NoCycle_mut.
 
-Require Import Eqdep_dec.
+From Stdlib Require Import Eqdep_dec.
 
 Theorem nat_dec (n m : nat) : {n = m} + {n <> m}.
 Proof. decide equality. Defined.
diff --git a/test-suite/nolam.v b/test-suite/nolam.v
index 5a72662b7..4528c93df 100644
--- a/test-suite/nolam.v
+++ b/test-suite/nolam.v
@@ -6,9 +6,9 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-Require Import Bvector List Relations.
+From Stdlib Require Import List Relations.
 From Equations Require Import Equations Signature.
-Require Import Utf8.
+From Stdlib Require Import Utf8.
 Import ListNotations.
 
 Equations f : forall {A : Type}, list A -> nat :=
diff --git a/test-suite/notations.v b/test-suite/notations.v
index c7894de3f..063cea384 100644
--- a/test-suite/notations.v
+++ b/test-suite/notations.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 Reserved Notation "x +++ y" (at level 50).
 
@@ -30,7 +30,7 @@ Equations rev {A} : list A -> list A :=
        { acc ++++ [] := acc;
          acc ++++ (x :: l') := (x :: acc) ++++ l' }.
 
-Require Import Arith NArith.
+From Stdlib Require Import Arith NArith.
 Local Open Scope N_scope.
 
 (** Parsing works with scopes as well *)
diff --git a/test-suite/rec.v b/test-suite/rec.v
index 39fd05e65..905293ce9 100644
--- a/test-suite/rec.v
+++ b/test-suite/rec.v
@@ -5,12 +5,12 @@
 (* This file is distributed under the terms of the                    *)
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
-Require Import Program Utf8.
+From Stdlib Require Import Program Utf8.
 From Equations.Prop Require Import Equations.
 
-Require Import Bvector List Relations.
-Require Import Arith Wf_nat.
-Require Import Lia.
+From Stdlib Require Import List Relations.
+From Stdlib Require Import Arith Wf_nat.
+From Stdlib Require Import Lia.
 
 Module RecRel.
   Unset Equations With Funext.
@@ -83,7 +83,7 @@ Inductive xor (A B : Prop) : Prop :=
 | xor_left : A -> not B -> xor A B
 | xor_right : B -> not A -> xor A B.
 
-Require Import Bool.
+From Stdlib Require Import Bool.
 Coercion Is_true : bool >-> Sortclass.
 
 Lemma xor_reflect (x y : bool) : reflect (xor x y) (xorb x y).
@@ -109,8 +109,8 @@ Proof with simpl; intros. intros.
   auto using Permutation_cons_app. elim H1.
 Qed.
 
-Require Import EquivDec.
-Require Import Permutation.
+From Stdlib Require Import EquivDec.
+From Stdlib Require Import Permutation.
 
 Module RecMeasure.
 
diff --git a/test-suite/rose.v b/test-suite/rose.v
index d2e320788..952c78c84 100644
--- a/test-suite/rose.v
+++ b/test-suite/rose.v
@@ -5,7 +5,7 @@
 (* begin hide *)
 From Equations.Prop Require Import Equations.
 
-Require Import Lia Utf8 List.
+From Stdlib Require Import Lia Utf8 List.
 Import ListNotations.
 Set Keyed Unification.
 
@@ -32,7 +32,7 @@ Section list_size.
   Qed.
 End list_size.
 
-Require Import List.
+From Stdlib Require Import List.
 (* end hide *)
 (** To demonstrate nested well-founded recursive definitions, we take a
   well-known example from the literature: rose trees.  We will define a
diff --git a/test-suite/scope.v b/test-suite/scope.v
index 1d75c58f9..2a207e6c2 100644
--- a/test-suite/scope.v
+++ b/test-suite/scope.v
@@ -8,7 +8,7 @@ From Equations.Prop Require Import Equations.
 From Stdlib Require Import Eqdep_dec.
 From Stdlib Require Import EquivDec.
 
-Require Import Arith.
+From Stdlib Require Import Arith.
 Derive Signature for eq.
 
 Definition scope := nat.
diff --git a/test-suite/terms.v b/test-suite/terms.v
index fa3edc68d..a36887fd3 100644
--- a/test-suite/terms.v
+++ b/test-suite/terms.v
@@ -5,12 +5,13 @@ Inductive term :=
 | App : term -> list term -> term
 | Lam : term -> term.
 
-Equations term_size (t : term) : nat :=
+#[derive(eliminator=no)] Equations term_size (t : term) : nat :=
 term_size (Var n) := 0;
 term_size (App f l) := S (List.fold_left (fun acc x => max acc (term_size x)) l (term_size f));
 term_size (Lam f) := S (term_size f).
 
 (** TODO: recognize recursive call under lambda abstraction *)
+#[derive(eliminator=no)]
 Equations subst (t : term) (k : nat) (u : term) : term :=
 subst t k (Var n) := if Nat.eqb k n then t else Var n;
 subst t k (App f l) := App (subst t k f) (List.map (fun x => subst t k x) l);
diff --git a/test-suite/wfnocycle.v b/test-suite/wfnocycle.v
index 7d229178e..7b439f252 100644
--- a/test-suite/wfnocycle.v
+++ b/test-suite/wfnocycle.v
@@ -1,13 +1,13 @@
 Set Warnings "-notation-overridden".
 From Equations.Prop Require Import Equations.
 
-Require Import Utf8 Arith Compare_dec List Lia.
-Require Import Relation_Operators.
+From Stdlib Require Import Utf8 Arith Compare_dec List Lia.
+From Stdlib Require Import Relation_Operators.
 Arguments clos_trans [A].
 Import Sigma_Notations.
 Set Equations Transparent.
 
-Require Import fin.
+From Equations.TestSuite Require Import fin.
 
 Equations lift_fin {n} (k : nat) (f : fin n) : fin (S n) :=
   lift_fin 0 f := fs f;
diff --git a/test-suite/yves.v b/test-suite/yves.v
index 05f827021..2ec95a215 100644
--- a/test-suite/yves.v
+++ b/test-suite/yves.v
@@ -1,4 +1,4 @@
-Require Import Arith.
+From Stdlib Require Import Arith.
 From Equations.Prop Require Import Equations.
 
 Inductive btree (T : Type) : Type :=
diff --git a/test-suite/zoe.v b/test-suite/zoe.v
index 882886923..f096cc3bb 100644
--- a/test-suite/zoe.v
+++ b/test-suite/zoe.v
@@ -1,6 +1,6 @@
 From Equations.Prop Require Import Equations.
 
-Require Import Arith List ListSet Lia Program.
+From Stdlib Require Import Arith List ListSet Lia Program.
 Import ListNotations.
 Set Keyed Unification.
  
diff --git a/theories/CoreTactics.v b/theories/CoreTactics.v
index 69944dbe1..2f6f65e9a 100644
--- a/theories/CoreTactics.v
+++ b/theories/CoreTactics.v
@@ -9,7 +9,7 @@
 (** Tactics supporting equations *)
 
 Require Export Equations.Init.
-Require Import Equations.Signature.
+From Equations Require Import Signature.
 
 Local Open Scope equations_scope.
 
diff --git a/theories/HoTT/Classes.v b/theories/HoTT/Classes.v
index fd5107d5f..40c82a16e 100644
--- a/theories/HoTT/Classes.v
+++ b/theories/HoTT/Classes.v
@@ -6,10 +6,10 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-Require Import Equations.Init Equations.CoreTactics.
+From Equations Require Import Init CoreTactics.
 Set Warnings "-notation-overridden".
-Require Import HoTT.Basics.Trunc HoTT.HSet.
-Require Import Equations.HoTT.Logic Equations.HoTT.Relation
+From Stdlib Require Import HoTT.Basics.Trunc HoTT.HSet.
+From Equations Require Import HoTT.Logic Equations.HoTT.Relation
         Equations.HoTT.Relation_Properties Equations.HoTT.WellFounded.
 
 Set Universe Polymorphism.
diff --git a/theories/HoTT/Constants.v b/theories/HoTT/Constants.v
index 7ce28c33a..059223cc4 100644
--- a/theories/HoTT/Constants.v
+++ b/theories/HoTT/Constants.v
@@ -1,7 +1,7 @@
 Set Warnings "-notation-overridden".
 
 From Equations Require Import Init.
-Require Import Equations.HoTT.Logic Equations.HoTT.DepElim
+From Equations Require Import HoTT.Logic Equations.HoTT.DepElim
         Equations.HoTT.EqDec Equations.HoTT.Classes.
 From HoTT Require Import Spaces.Nat.
 
diff --git a/theories/HoTT/DepElim.v b/theories/HoTT/DepElim.v
index 21411cfd0..b657fad0c 100644
--- a/theories/HoTT/DepElim.v
+++ b/theories/HoTT/DepElim.v
@@ -10,12 +10,12 @@
 
 Set Warnings "-notation-overridden".
 
-Require Import Stdlib.Program.Tactics.
+From Stdlib Require Import Program.Tactics.
 Require Export Equations.Init.
-Require Import Equations.Signature Equations.CoreTactics.
-Require Import Equations.HoTT.Logic.
-Require Import Equations.HoTT.Classes.
-Require Import Equations.HoTT.EqDec.
+From Equations Require Import Signature CoreTactics.
+From Equations Require Import HoTT.Logic.
+From Equations Require Import HoTT.Classes.
+From Equations Require Import HoTT.EqDec.
 
 Set Universe Polymorphism.
 
diff --git a/theories/HoTT/EqDec.v b/theories/HoTT/EqDec.v
index 54865b812..745ce4555 100644
--- a/theories/HoTT/EqDec.v
+++ b/theories/HoTT/EqDec.v
@@ -8,9 +8,9 @@
 
 Set Warnings "-notation-overridden".
 
-Require Import Equations.Init.
-Require Import Equations.HoTT.Logic.
-Require Import Equations.HoTT.Classes.
+From Equations Require Import Init.
+From Equations Require Import HoTT.Logic.
+From Equations Require Import HoTT.Classes.
 
 (** Decidable equality.
 
@@ -232,7 +232,7 @@ Definition apd_eq {A} {x y : A} (p : x = y) {z} (q : z = x) :
   transport (@paths A z) p q = q @ p.
 Proof. now destruct p, q. Defined.
 
-Require Import HoTT.Basics.Trunc.
+From Stdlib Require Import HoTT.Basics.Trunc.
 
 Lemma hprop_hset {A} (h : IsHProp A) : IsHSet A.
 Proof.
diff --git a/theories/HoTT/EqDecInstances.v b/theories/HoTT/EqDecInstances.v
index 634ae61a4..83df3af7d 100644
--- a/theories/HoTT/EqDecInstances.v
+++ b/theories/HoTT/EqDecInstances.v
@@ -7,7 +7,7 @@
 (**********************************************************************)
 Set Warnings "-notation-overridden".
 From Equations Require Import Init.
-Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.DepElim
+From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.DepElim
         Equations.HoTT.Constants
         Equations.HoTT.Tactics Equations.HoTT.EqDec Equations.HoTT.NoConfusion.
 From HoTT Require Import Spaces.List.Core.
diff --git a/theories/HoTT/FunctionalInduction.v b/theories/HoTT/FunctionalInduction.v
index fdc24cc47..353d36954 100644
--- a/theories/HoTT/FunctionalInduction.v
+++ b/theories/HoTT/FunctionalInduction.v
@@ -7,9 +7,9 @@
 (**********************************************************************)
 
 Set Warnings "-notation-overridden".
-Require Import Equations.CoreTactics.
-Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.DepElim.
-Require Import HoTT.Spaces.Nat.
+From Equations Require Import CoreTactics.
+From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.DepElim.
+From Stdlib Require Import HoTT.Spaces.Nat.
 
 Local Open Scope nat_scope.
 Local Open Scope equations_scope.
diff --git a/theories/HoTT/Loader.v b/theories/HoTT/Loader.v
index 6a5813f9b..4f2f13053 100644
--- a/theories/HoTT/Loader.v
+++ b/theories/HoTT/Loader.v
@@ -12,13 +12,13 @@
 
 Set Warnings "-notation-overridden".
 From Equations Require Export Init Signature.
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 Require Export Equations.HoTT.Logic Equations.HoTT.Classes.
-Require Import Equations.HoTT.WellFounded.
-Require Import Equations.HoTT.DepElim Equations.HoTT.EqDec Equations.HoTT.Constants.
+From Equations Require Import HoTT.WellFounded.
+From Equations Require Import HoTT.DepElim Equations.HoTT.EqDec Equations.HoTT.Constants.
 Require Export Equations.HoTT.EqDecInstances.
 Require Export Equations.HoTT.NoConfusion.
-Require Import Equations.HoTT.Subterm.
+From Equations Require Import HoTT.Subterm.
 Require Export Equations.HoTT.Tactics.
 Require Export Equations.HoTT.FunctionalInduction. (* funelim tactic *)
 
diff --git a/theories/HoTT/Logic.v b/theories/HoTT/Logic.v
index d161be9dc..fecb33d55 100644
--- a/theories/HoTT/Logic.v
+++ b/theories/HoTT/Logic.v
@@ -23,7 +23,7 @@ Register ap as core.identity.congr.
 
 Definition path_inspect {A : Type} (x : A) : { y | paths x y } := (x ; idpath).
 
-Require Import HoTT.Types.Bool.
+From Stdlib Require Import HoTT.Types.Bool.
 (* For compatibility with Coq's [induction] *)
 Definition Bool_rect := Bool_ind.
 
diff --git a/theories/HoTT/NoConfusion.v b/theories/HoTT/NoConfusion.v
index 292041ac7..88f6263db 100644
--- a/theories/HoTT/NoConfusion.v
+++ b/theories/HoTT/NoConfusion.v
@@ -13,10 +13,10 @@
 Set Warnings "-notation-overridden".
 
 From Equations Require Import Init Signature.
-Require Import Equations.CoreTactics.
-Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Constants.
-Require Import Equations.HoTT.DepElim Equations.HoTT.Tactics.
-Require Import HoTT.Spaces.List.Core.
+From Equations Require Import CoreTactics.
+From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Constants.
+From Equations Require Import HoTT.DepElim Equations.HoTT.Tactics.
+From Stdlib Require Import HoTT.Spaces.List.Core.
 
 
 (** Parameterized inductive types just need NoConfusion. *)
diff --git a/theories/HoTT/Relation.v b/theories/HoTT/Relation.v
index 5aa424cec..14df41353 100644
--- a/theories/HoTT/Relation.v
+++ b/theories/HoTT/Relation.v
@@ -11,7 +11,7 @@
 From Equations Require Import Init.
 
 Set Warnings "-notation-overridden".
-Require Import Equations.HoTT.Logic.
+From Equations Require Import HoTT.Logic.
 Require Export HoTT.Basics.Iff.
 
 Local Open Scope equations_scope.
diff --git a/theories/HoTT/Relation_Properties.v b/theories/HoTT/Relation_Properties.v
index a8fa236dc..eceb0a62b 100644
--- a/theories/HoTT/Relation_Properties.v
+++ b/theories/HoTT/Relation_Properties.v
@@ -16,9 +16,9 @@
 
 Set Warnings "-notation-overridden".
 
-Require Import Equations.Init.
-Require Import Equations.HoTT.Logic.
-Require Import Equations.HoTT.Relation.
+From Equations Require Import Init.
+From Equations Require Import HoTT.Logic.
+From Equations Require Import HoTT.Relation.
 
 Import Sigma_Notations.
 
diff --git a/theories/HoTT/Subterm.v b/theories/HoTT/Subterm.v
index 422497f6a..fe96ef782 100644
--- a/theories/HoTT/Subterm.v
+++ b/theories/HoTT/Subterm.v
@@ -9,8 +9,8 @@
 Set Warnings "-notation-overridden".
 
 From Equations Require Import Init Signature.
-Require Import Equations.CoreTactics.
-Require Import Equations.HoTT.Logic
+From Equations Require Import CoreTactics.
+From Equations Require Import HoTT.Logic
         Equations.HoTT.Classes Equations.HoTT.EqDec
         Equations.HoTT.Relation
         Equations.HoTT.WellFounded
diff --git a/theories/HoTT/Tactics.v b/theories/HoTT/Tactics.v
index 4340ddbd6..d9733215b 100644
--- a/theories/HoTT/Tactics.v
+++ b/theories/HoTT/Tactics.v
@@ -7,20 +7,19 @@
 (**********************************************************************)
 
 Set Warnings "-notation-overridden".
-Require Import Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.DepElim
-        Equations.HoTT.Subterm Equations.HoTT.EqDec
-        Equations.HoTT.WellFounded Equations.HoTT.FunctionalInduction.
+From Equations Require Import CoreTactics.
+From Equations.HoTT Require Import Logic DepElim Subterm EqDec WellFounded FunctionalInduction.
 
-Ltac Equations.Init.simpl_equations ::= Equations.HoTT.DepElim.simpl_equations.
-Ltac Equations.Init.simplify_equalities ::= Equations.HoTT.DepElim.simplify_dep_elim.
+Ltac Equations.Init.simpl_equations ::= DepElim.simpl_equations.
+Ltac Equations.Init.simplify_equalities ::= DepElim.simplify_dep_elim.
 
 Ltac Equations.Init.depelim H ::= dependent elimination H; cbn in *.
-Ltac Equations.Init.depind H ::= Equations.HoTT.DepElim.depind H.
-Ltac Equations.Init.simp_IHs_tac ::= Equations.HoTT.FunctionalInduction.simplify_IHs_call.
-Ltac Equations.Init.funelim_constr_as H H' tac ::= Equations.HoTT.FunctionalInduction.funelim_constr_as H H' tac.
-Ltac Equations.Init.apply_funelim H ::= Equations.HoTT.FunctionalInduction.apply_funelim H.
+Ltac Equations.Init.depind H ::= DepElim.depind H.
+Ltac Equations.Init.simp_IHs_tac ::= FunctionalInduction.simplify_IHs_call.
+Ltac Equations.Init.funelim_constr_as H H' tac ::= FunctionalInduction.funelim_constr_as H H' tac.
+Ltac Equations.Init.apply_funelim H ::= FunctionalInduction.apply_funelim H.
 
-Ltac Equations.Init.noconf H ::= Equations.HoTT.DepElim.noconf H.
+Ltac Equations.Init.noconf H ::= DepElim.noconf H.
 
 Create HintDb solve_subterm discriminated.
 
@@ -34,8 +33,8 @@ Ltac solve_subterm := intros;
   simplify_dep_elim; try typeclasses eauto with solve_subterm.
 
 Ltac Equations.Init.solve_subterm ::= solve_subterm.
-Ltac Equations.Init.unfold_recursor ::= Equations.HoTT.Subterm.unfold_recursor.
-Ltac Equations.Init.unfold_recursor_ext ::= Equations.HoTT.Subterm.unfold_recursor_ext.
+Ltac Equations.Init.unfold_recursor ::= Subterm.unfold_recursor.
+Ltac Equations.Init.unfold_recursor_ext ::= Subterm.unfold_recursor_ext.
 
 Ltac solve_noconf_inv_eq a b :=
   destruct_sigma a; destruct_sigma b;
diff --git a/theories/HoTT/Telescopes.v b/theories/HoTT/Telescopes.v
index 09dbf3a86..4627d7482 100644
--- a/theories/HoTT/Telescopes.v
+++ b/theories/HoTT/Telescopes.v
@@ -1,11 +1,11 @@
 Set Warnings "-notation-overridden".
-Require Import Equations.HoTT.Loader.
-Require Import Equations.HoTT.Logic.
-Require Import Equations.HoTT.WellFounded.
-Require Import Equations.HoTT.DepElim.
-Require Import Equations.HoTT.Tactics.
-Require Import Equations.HoTT.FunctionalInduction.
-Require Import Equations.HoTT.Subterm.
+From Equations Require Import HoTT.Loader.
+From Equations Require Import HoTT.Logic.
+From Equations Require Import HoTT.WellFounded.
+From Equations Require Import HoTT.DepElim.
+From Equations Require Import HoTT.Tactics.
+From Equations Require Import HoTT.FunctionalInduction.
+From Equations Require Import HoTT.Subterm.
 From HoTT Require Import Basics.Tactics.
 
 (** Telescopes: allows treating variable arity fixpoints *)
diff --git a/theories/HoTT/WellFounded.v b/theories/HoTT/WellFounded.v
index 515321945..fdc427056 100644
--- a/theories/HoTT/WellFounded.v
+++ b/theories/HoTT/WellFounded.v
@@ -1,8 +1,8 @@
 Set Warnings "-notation-overridden".
-Require Import Equations.Init Equations.CoreTactics.
-Require Import Equations.HoTT.Logic
+From Equations Require Import Init CoreTactics.
+From Equations Require Import HoTT.Logic
         Equations.HoTT.Relation Equations.HoTT.Relation_Properties.
-Require Import HoTT.Basics.Tactics.
+From Stdlib Require Import HoTT.Basics.Tactics.
 
 Set Universe Polymorphism.
 Import Sigma_Notations.
diff --git a/theories/HoTT/WellFoundedInstances.v b/theories/HoTT/WellFoundedInstances.v
index 00d934dd3..01d4f8ea3 100644
--- a/theories/HoTT/WellFoundedInstances.v
+++ b/theories/HoTT/WellFoundedInstances.v
@@ -1,5 +1,5 @@
 Set Warnings "-notation-overridden".
-Require Import Equations.HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded.
+From Equations Require Import HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded.
 From HoTT Require Import Spaces.Nat.
 
 Section Lt.
diff --git a/theories/Prop/Classes.v b/theories/Prop/Classes.v
index 385719c1e..3d9350170 100644
--- a/theories/Prop/Classes.v
+++ b/theories/Prop/Classes.v
@@ -6,7 +6,7 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-Require Import Equations.Init Equations.CoreTactics.
+From Equations Require Import Init CoreTactics.
 From Stdlib Require Import Extraction Relation_Definitions.
 From Equations.Prop Require Import Logic.
 
diff --git a/theories/Prop/DepElim.v b/theories/Prop/DepElim.v
index 54b66f749..e350f5da9 100644
--- a/theories/Prop/DepElim.v
+++ b/theories/Prop/DepElim.v
@@ -8,10 +8,10 @@
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
-Require Import Stdlib.Program.Tactics.
+From Stdlib Require Import Program.Tactics.
 Require Export Equations.Init.
-Require Import Equations.CoreTactics.
-Require Import Equations.Signature.
+From Equations Require Import CoreTactics.
+From Equations Require Import Signature.
 From Equations.Prop Require Import Logic.
 From Equations.Prop Require Import Classes.
 From Equations.Prop Require Import EqDec.
diff --git a/theories/Prop/EqDec.v b/theories/Prop/EqDec.v
index a4a5eb0bd..d7a461a20 100644
--- a/theories/Prop/EqDec.v
+++ b/theories/Prop/EqDec.v
@@ -6,7 +6,7 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-Require Import Equations.Init.
+From Equations Require Import Init.
 From Equations.Prop Require Import Classes.
 
 (** Decidable equality.
diff --git a/theories/Prop/Equations.v b/theories/Prop/Equations.v
index 6f6d4213f..ba69a6eeb 100644
--- a/theories/Prop/Equations.v
+++ b/theories/Prop/Equations.v
@@ -13,7 +13,7 @@ From Equations.Prop Require Import Telescopes.
 
 #[export] Existing Instance wf_tele_measure.
 
-Require Import Program.Tactics.
+From Stdlib Require Import Program.Tactics.
 
 (* program_solve_wf launches auto on well-founded and propositional (i.e. in Prop) goals *)
 
diff --git a/theories/Prop/FunctionalInduction.v b/theories/Prop/FunctionalInduction.v
index cc400f15e..375954a04 100644
--- a/theories/Prop/FunctionalInduction.v
+++ b/theories/Prop/FunctionalInduction.v
@@ -6,7 +6,7 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 From Equations.Prop Require Import Logic Classes EqDec DepElim.
 
 (** The tactic [funind c Hc] applies functional induction on the application 
diff --git a/theories/Prop/Loader.v b/theories/Prop/Loader.v
index ea08f09e0..d29d29c64 100644
--- a/theories/Prop/Loader.v
+++ b/theories/Prop/Loader.v
@@ -8,13 +8,13 @@
 
 (** The set of libraries required to run Equations with all features. *)
 
-Require Import Extraction.
+From Stdlib Require Import Extraction.
 
 (** This exports tactics *)
 Declare ML Module "rocq-equations.plugin".
 
 From Equations Require Export Init Signature.
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 Require Export Equations.Prop.SigmaNotations.
 Require Export Equations.Prop.Classes.
 From Equations.Prop Require Import DepElim Constants.
diff --git a/theories/Prop/NoConfusion.v b/theories/Prop/NoConfusion.v
index 1fd77cf86..2613091e3 100644
--- a/theories/Prop/NoConfusion.v
+++ b/theories/Prop/NoConfusion.v
@@ -14,7 +14,7 @@ Set Warnings "-deprecated-since-8.20".
 From Stdlib Require Import Program.Tactics Bvector List.
 Set Warnings "deprecated-since-8.20".
 From Equations Require Import Init Signature.
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 From Equations.Prop Require Import Classes EqDec Constants.
 From Equations.Prop Require Import DepElim Tactics.
 
diff --git a/theories/Prop/NoCycle.v b/theories/Prop/NoCycle.v
index 0d41407a7..2f2d90ace 100644
--- a/theories/Prop/NoCycle.v
+++ b/theories/Prop/NoCycle.v
@@ -55,7 +55,7 @@ Proof with trivial.
         + firstorder. }
 Qed.
 
-Require Import CRelationClasses.
+From Stdlib Require Import CRelationClasses.
 
 #[export]
 Instance nlt_refl : Reflexive nlt.
diff --git a/theories/Prop/Subterm.v b/theories/Prop/Subterm.v
index 129d4ab4e..3424f248c 100644
--- a/theories/Prop/Subterm.v
+++ b/theories/Prop/Subterm.v
@@ -12,7 +12,7 @@ From Stdlib Require Import Relation_Operators Lexicographic_Product Wf_nat.
 From Stdlib Require Export Program.Wf FunctionalExtensionality.
 
 From Equations Require Import Init Signature.
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 From Equations.Prop Require Import Classes EqDec DepElim Constants.
 
 Generalizable Variables A R S B.
diff --git a/theories/Prop/Tactics.v b/theories/Prop/Tactics.v
index fed1f13ff..efd7ba78d 100644
--- a/theories/Prop/Tactics.v
+++ b/theories/Prop/Tactics.v
@@ -5,17 +5,17 @@
 (* This file is distributed under the terms of the                    *)
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
-Require Import Equations.CoreTactics Equations.Prop.Classes Equations.Prop.DepElim
-        Equations.Prop.Subterm Equations.Prop.FunctionalInduction.
-
-Ltac Equations.Init.simpl_equations ::= Equations.Prop.DepElim.simpl_equations.
-Ltac Equations.Init.simplify_equalities ::= Equations.Prop.DepElim.simplify_dep_elim.
-Ltac Equations.Init.depelim H ::= Equations.Prop.DepElim.depelim H.
-Ltac Equations.Init.depind H ::= Equations.Prop.DepElim.depind H.
-Ltac Equations.Init.noconf H ::= Equations.Prop.DepElim.noconf H.
-Ltac Equations.Init.simp_IHs_tac ::= Equations.Prop.FunctionalInduction.simplify_IHs_call.
-Ltac Equations.Init.funelim_constr_as x H simp_IHs ::= Equations.Prop.FunctionalInduction.funelim_constr_as x H simp_IHs.
-Ltac Equations.Init.apply_funelim H ::= Equations.Prop.FunctionalInduction.apply_funelim H.
+From Equations Require Import CoreTactics.
+From Equations.Prop Require Import Classes DepElim Subterm FunctionalInduction.
+
+Ltac Equations.Init.simpl_equations ::= DepElim.simpl_equations.
+Ltac Equations.Init.simplify_equalities ::= DepElim.simplify_dep_elim.
+Ltac Equations.Init.depelim H ::= DepElim.depelim H.
+Ltac Equations.Init.depind H ::= DepElim.depind H.
+Ltac Equations.Init.noconf H ::= DepElim.noconf H.
+Ltac Equations.Init.simp_IHs_tac ::= FunctionalInduction.simplify_IHs_call.
+Ltac Equations.Init.funelim_constr_as x H simp_IHs ::= FunctionalInduction.funelim_constr_as x H simp_IHs.
+Ltac Equations.Init.apply_funelim H ::= FunctionalInduction.apply_funelim H.
 
 (** Tactic to solve EqDec goals, destructing recursive calls for the recursive
   structure of the type and calling instances of eq_dec on other types. *)
@@ -64,9 +64,9 @@ Ltac eqdec_proof := try red; intros;
   end; try solve[left; reflexivity | right; red; simplify_dep_elim].
 
 Ltac Equations.Init.solve_eqdec ::= eqdec_proof.
-Ltac Equations.Init.solve_subterm ::= Equations.Prop.Subterm.solve_subterm.
-Ltac Equations.Init.unfold_recursor ::= Equations.Prop.Subterm.unfold_recursor.
-Ltac Equations.Init.unfold_recursor_ext ::= Equations.Prop.Subterm.unfold_recursor_ext.
+Ltac Equations.Init.solve_subterm ::= Subterm.solve_subterm.
+Ltac Equations.Init.unfold_recursor ::= Subterm.unfold_recursor.
+Ltac Equations.Init.unfold_recursor_ext ::= Subterm.unfold_recursor_ext.
 
 Ltac solve_noconf_prf := intros;
   on_last_hyp ltac:(fun id => destruct id) ; (* Subtitute a = b *)
diff --git a/theories/Type/All.v b/theories/Type/All.v
index f76d841ff..f4cb3b245 100644
--- a/theories/Type/All.v
+++ b/theories/Type/All.v
@@ -15,7 +15,7 @@ Require Export Equations.Type.Loader.
 Require Export Equations.Type.Telescopes.
 Require Export Equations.Type.WellFoundedInstances.
 
-Global Obligation Tactic := Equations.CoreTactics.equations_simpl.
+Global Obligation Tactic := CoreTactics.equations_simpl.
 
 (** Tactic to solve well-founded proof obligations by default *)
 
diff --git a/theories/Type/Classes.v b/theories/Type/Classes.v
index a19912372..2eedee000 100644
--- a/theories/Type/Classes.v
+++ b/theories/Type/Classes.v
@@ -7,7 +7,7 @@
 (**********************************************************************)
 
 From Stdlib Require Import Extraction CRelationClasses.
-Require Import Equations.Init Equations.CoreTactics.
+From Equations Require Import Init CoreTactics.
 Set Warnings "-notation-overridden".
 From Equations.Type Require Import Logic Relation Relation_Properties WellFounded.
 
diff --git a/theories/Type/DepElim.v b/theories/Type/DepElim.v
index e79dcfc1a..6eaa6f670 100644
--- a/theories/Type/DepElim.v
+++ b/theories/Type/DepElim.v
@@ -10,9 +10,9 @@
 
 Set Warnings "-notation-overridden".
 
-Require Import Stdlib.Program.Tactics.
+From Stdlib Require Import Program.Tactics.
 Require Export Equations.Init.
-Require Import Equations.Signature Equations.CoreTactics.
+From Equations Require Import Signature CoreTactics.
 From Equations.Type Require Import Logic.
 From Equations.Type Require Import Classes.
 From Equations.Type Require Import EqDec.
diff --git a/theories/Type/EqDec.v b/theories/Type/EqDec.v
index 2f9a8012f..ed4a9b45d 100644
--- a/theories/Type/EqDec.v
+++ b/theories/Type/EqDec.v
@@ -8,7 +8,7 @@
 
 Set Warnings "-notation-overridden".
 
-Require Import Equations.Init.
+From Equations Require Import Init.
 From Equations.Type Require Import Logic.
 From Equations.Type Require Import Classes.
 
diff --git a/theories/Type/FunctionalInduction.v b/theories/Type/FunctionalInduction.v
index a3331c5a3..3d290df43 100644
--- a/theories/Type/FunctionalInduction.v
+++ b/theories/Type/FunctionalInduction.v
@@ -7,7 +7,7 @@
 (**********************************************************************)
 
 Set Warnings "-notation-overridden".
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 From Equations.Type Require Import Logic Classes EqDec DepElim.
 
 Set Universe Polymorphism.
diff --git a/theories/Type/Loader.v b/theories/Type/Loader.v
index 4e029e1c7..e19b44474 100644
--- a/theories/Type/Loader.v
+++ b/theories/Type/Loader.v
@@ -8,14 +8,14 @@
 
 (** The set of libraries required to run Equations with all features. *)
 
-Require Import Extraction.
+From Stdlib Require Import Extraction.
 
 (** This exports tactics *)
 Declare ML Module "rocq-equations.plugin".
 
 Set Warnings "-notation-overridden".
 From Equations Require Export Init Signature.
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 From Equations.Type Require Export Logic Classes.
 From Equations.Type Require Import WellFounded.
 From Equations.Type Require Import DepElim EqDec Constants.
diff --git a/theories/Type/NoConfusion.v b/theories/Type/NoConfusion.v
index f9ac69c5c..803bf4d83 100644
--- a/theories/Type/NoConfusion.v
+++ b/theories/Type/NoConfusion.v
@@ -11,7 +11,7 @@
    on some equation. *)
 
 From Equations Require Import Init Signature.
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 From Equations.Type Require Import Classes EqDec Constants.
 From Equations.Type Require Import DepElim Tactics.
 
diff --git a/theories/Type/Relation_Properties.v b/theories/Type/Relation_Properties.v
index b5ca21aff..4e6718297 100644
--- a/theories/Type/Relation_Properties.v
+++ b/theories/Type/Relation_Properties.v
@@ -16,8 +16,8 @@
 
 Set Warnings "-notation-overridden".
 
-Require Import CRelationClasses.
-Require Import Equations.Init.
+From Stdlib Require Import CRelationClasses.
+From Equations Require Import Init.
 From Equations.Type Require Import Logic.
 From Equations.Type Require Import Relation.
 
diff --git a/theories/Type/Subterm.v b/theories/Type/Subterm.v
index 7c1848243..6af575389 100644
--- a/theories/Type/Subterm.v
+++ b/theories/Type/Subterm.v
@@ -9,7 +9,7 @@
 Set Warnings "-notation-overridden".
 
 From Equations Require Import Init Signature.
-Require Import Equations.CoreTactics.
+From Equations Require Import CoreTactics.
 From Equations.Type Require Import Logic Classes EqDec
   Relation FunctionalExtensionality WellFounded DepElim Constants.
 
diff --git a/theories/Type/Tactics.v b/theories/Type/Tactics.v
index 67ac9c7f1..c33e3731e 100644
--- a/theories/Type/Tactics.v
+++ b/theories/Type/Tactics.v
@@ -7,19 +7,19 @@
 (**********************************************************************)
 
 Set Warnings "-notation-overridden".
-Require Import Equations.CoreTactics Equations.Type.Logic Equations.Type.DepElim Equations.Type.EqDec
-        Equations.Type.Subterm Equations.Type.WellFounded Equations.Type.FunctionalInduction.
+From Equations Require Import CoreTactics.
+From Equations.Type Require Import Logic DepElim EqDec Subterm WellFounded FunctionalInduction.
 
-Ltac Equations.Init.simpl_equations ::= Equations.Type.DepElim.simpl_equations.
-Ltac Equations.Init.simplify_equalities ::= Equations.Type.DepElim.simplify_dep_elim.
+Ltac Equations.Init.simpl_equations ::= DepElim.simpl_equations.
+Ltac Equations.Init.simplify_equalities ::= DepElim.simplify_dep_elim.
 
 Ltac Equations.Init.depelim H ::= dependent elimination H; cbn in *.
-Ltac Equations.Init.depind H ::= Equations.Type.DepElim.depind H.
-Ltac Equations.Init.simp_IHs_tac ::= Equations.Type.FunctionalInduction.simplify_IHs_call.
-Ltac Equations.Init.funelim_constr_as H H' tac ::= Equations.Type.FunctionalInduction.funelim_constr_as H H' tac.
-Ltac Equations.Init.apply_funelim H ::= Equations.Type.FunctionalInduction.apply_funelim H.
+Ltac Equations.Init.depind H ::= DepElim.depind H.
+Ltac Equations.Init.simp_IHs_tac ::= FunctionalInduction.simplify_IHs_call.
+Ltac Equations.Init.funelim_constr_as H H' tac ::= FunctionalInduction.funelim_constr_as H H' tac.
+Ltac Equations.Init.apply_funelim H ::= FunctionalInduction.apply_funelim H.
 
-Ltac Equations.Init.noconf H ::= Equations.Type.DepElim.noconf H.
+Ltac Equations.Init.noconf H ::= DepElim.noconf H.
 
 Create HintDb solve_subterm discriminated.
 
@@ -36,8 +36,8 @@ Ltac solve_subterm := intros;
 
 Ltac Equations.Init.solve_subterm ::= solve_subterm.
 Ltac Equations.Init.solve_eqdec ::= eqdec_proof.
-Ltac Equations.Init.unfold_recursor ::= Equations.Type.Subterm.unfold_recursor.
-Ltac Equations.Init.unfold_recursor_ext ::= Equations.Type.Subterm.unfold_recursor_ext.
+Ltac Equations.Init.unfold_recursor ::= Subterm.unfold_recursor.
+Ltac Equations.Init.unfold_recursor_ext ::= Subterm.unfold_recursor_ext.
 
 Ltac solve_noconf_prf := intros;
   on_last_hyp ltac:(fun id => destruct id) ; (* Subtitute a = b *)
diff --git a/theories/Type/WellFounded.v b/theories/Type/WellFounded.v
index 196109b75..860efeb2c 100644
--- a/theories/Type/WellFounded.v
+++ b/theories/Type/WellFounded.v
@@ -1,6 +1,6 @@
 Set Warnings "-notation-overridden".
 From Stdlib Require Import Extraction CRelationClasses.
-Require Import Equations.Init Equations.CoreTactics.
+From Equations Require Import Init CoreTactics.
 From Equations.Type Require Import Logic FunctionalExtensionality Relation Relation_Properties.
 
 Set Universe Polymorphism.