diff --git a/_RocqProject b/_RocqProject
index b85bd434..cd5d98f7 100644
--- a/_RocqProject
+++ b/_RocqProject
@@ -1,7 +1,6 @@
 # [tag:flags]
 -arg "-set 'Default Goal Selector=!'"
--arg "-set 'Loose Hint Behavior=Strict'"
 -arg "-set 'Primitive Projections'"
 -arg "-set 'Printing Projections'"
--arg "-unset 'Printing Primitive Projection Parameters'"
+-arg "-w +default"
 -Q proofs_rocq main
diff --git a/proofs_rocq/category_theory/arrow.v b/proofs_rocq/category_theory/arrow.v
index 209ea7e5..0659371d 100644
--- a/proofs_rocq/category_theory/arrow.v
+++ b/proofs_rocq/category_theory/arrow.v
@@ -6,8 +6,6 @@
 (********************)
 (********************)
 
-Require Import Stdlib.Classes.Morphisms.
-Require Import Stdlib.Classes.Morphisms_Prop.
 Require Import main.category_theory.category.
 Require Import main.tactics.
 
diff --git a/proofs_rocq/category_theory/coproduct.v b/proofs_rocq/category_theory/coproduct.v
index e20ae8a2..b1240972 100644
--- a/proofs_rocq/category_theory/coproduct.v
+++ b/proofs_rocq/category_theory/coproduct.v
@@ -6,7 +6,6 @@
 (************************)
 (************************)
 
-Require Import Stdlib.Classes.Morphisms.
 Require Import main.category_theory.arrow.
 Require Import main.category_theory.category.
 Require Import main.category_theory.initial.
diff --git a/proofs_rocq/category_theory/object.v b/proofs_rocq/category_theory/object.v
index 1c1cb3de..f36a907a 100644
--- a/proofs_rocq/category_theory/object.v
+++ b/proofs_rocq/category_theory/object.v
@@ -6,7 +6,6 @@
 (*********************)
 (*********************)
 
-Require Import Stdlib.Classes.Morphisms.
 Require Import main.category_theory.arrow.
 Require Import main.category_theory.category.
 Require Import main.tactics.
diff --git a/proofs_rocq/category_theory/terminal.v b/proofs_rocq/category_theory/terminal.v
index 62e3895b..cd2e5eb0 100644
--- a/proofs_rocq/category_theory/terminal.v
+++ b/proofs_rocq/category_theory/terminal.v
@@ -6,7 +6,6 @@
 (******************************)
 (******************************)
 
-Require Import Stdlib.Classes.Morphisms.
 Require Import main.category_theory.category.
 Require Import main.category_theory.initial.
 Require Import main.category_theory.object.
diff --git a/proofs_rocq/icbics/icbics.v b/proofs_rocq/icbics/icbics.v
index 1db3fc18..0bd5b725 100644
--- a/proofs_rocq/icbics/icbics.v
+++ b/proofs_rocq/icbics/icbics.v
@@ -23,6 +23,7 @@ Require Import Stdlib.Arith.Compare_dec.
 Require Import Stdlib.Lists.List.
 Require Import Stdlib.Sorting.Permutation.
 Require Import Stdlib.Sorting.Sorted.
+Require Import Stdlib.Vectors.FinFun.
 Require Import main.tactics.
 
 Import Stdlib.Arith.PeanoNat.Nat.
@@ -156,7 +157,6 @@ Proof.
   induction l; search; intros.
   - destruct j; search.
   - destruct i; destruct j; search.
-    apply IHl; search.
 Qed.
 
 #[local] Hint Resolve nth_firstn : main.
@@ -169,9 +169,6 @@ Proof.
   intros.
   outro i.
   induction l; intros; destruct i; search.
-  change (firstn (S i) (a :: l) ++ [nth (S i) (a :: l) d])
-    with (a :: firstn i l ++ [nth i l d]).
-  rewrite IHl; search.
 Qed.
 
 #[local] Hint Resolve cons_firstn_nth : main.
@@ -439,8 +436,6 @@ Proof.
   unfold for_loop.
   change (length l1) with n1.
   induction n1; search.
-  apply H0; search.
-  apply IHn1; search.
 Qed.
 
 (* Facts about `sort` *)
diff --git a/proofs_rocq/kleene/kleene_data.v b/proofs_rocq/kleene/kleene_data.v
index 29f0d2fb..41ff9c9a 100644
--- a/proofs_rocq/kleene/kleene_data.v
+++ b/proofs_rocq/kleene/kleene_data.v
@@ -6,6 +6,8 @@
 (****************************************************************)
 (****************************************************************)
 
+Require Import main.tactics.
+
 Module Type KleeneData.
   (*
     Assumption: Let (`T`, `Leq`) be a partially ordered set, or poset. A poset
diff --git a/proofs_rocq/stlc/name.v b/proofs_rocq/stlc/name.v
index 047e23a9..2e0f914b 100644
--- a/proofs_rocq/stlc/name.v
+++ b/proofs_rocq/stlc/name.v
@@ -6,7 +6,6 @@
 (*******************************************)
 (*******************************************)
 
-Require Import Stdlib.Arith.Peano_dec.
 Require Import main.tactics.
 
 Module Type NameSig.
diff --git a/proofs_rocq/system_f/context.v b/proofs_rocq/system_f/context.v
index 897bd012..0672874e 100644
--- a/proofs_rocq/system_f/context.v
+++ b/proofs_rocq/system_f/context.v
@@ -6,7 +6,6 @@
 (*****************************)
 (*****************************)
 
-Require Import Stdlib.Bool.Bool.
 Require Import Stdlib.Lists.List.
 Require Import main.system_f.free_var.
 Require Import main.system_f.local_closure.
diff --git a/proofs_rocq/system_f/local_closure.v b/proofs_rocq/system_f/local_closure.v
index a46c35f1..f6a18f7a 100644
--- a/proofs_rocq/system_f/local_closure.v
+++ b/proofs_rocq/system_f/local_closure.v
@@ -70,7 +70,6 @@ Theorem t_local_closure_monotonic :
   TLocallyClosed t i2.
 Proof.
   clean. outro i2 H. induction H0; search.
-  clean. apply tlc_for_all. apply IHTLocallyClosed. search.
 Qed.
 
 (* Don't add a resolve hint because `eapply` has a hard time guessing `i1`. *)
@@ -85,8 +84,6 @@ Proof.
   clean. outro ie2 it2 H H0.
   induction H1; search; constructor; search; clean.
   - apply t_local_closure_monotonic with (i1 := nt); search.
-  - apply IHELocallyClosed; search.
-  - apply IHELocallyClosed; search.
   - apply t_local_closure_monotonic with (i1 := nt); search.
 Qed.
 
diff --git a/proofs_rocq/system_f/name.v b/proofs_rocq/system_f/name.v
index abbd7f8a..43a38a9b 100644
--- a/proofs_rocq/system_f/name.v
+++ b/proofs_rocq/system_f/name.v
@@ -6,7 +6,6 @@
 (*******************************************)
 (*******************************************)
 
-Require Import Stdlib.Arith.Peano_dec.
 Require Import Stdlib.Lists.List.
 Require Import main.tactics.
 
diff --git a/proofs_rocq/system_f/opening.v b/proofs_rocq/system_f/opening.v
index 9c67a26a..448723ce 100644
--- a/proofs_rocq/system_f/opening.v
+++ b/proofs_rocq/system_f/opening.v
@@ -231,10 +231,7 @@ Proof.
   induction H2; search; clean.
   specialize (IHTLocallyClosed t2 (S i)).
   feed IHTLocallyClosed.
-  - apply t_local_closure_monotonic with (i1 := i); search.
-  - apply tlc_for_all.
-    apply IHTLocallyClosed.
-    search.
+  apply t_local_closure_monotonic with (i1 := i); search.
 Qed.
 
 Hint Resolve locally_closed_open_for_all : main.
@@ -274,9 +271,7 @@ Proof.
     apply t_local_closure_monotonic with (i1 := nt); search.
   - specialize (IHELocallyClosed t0 (S it)).
     feed IHELocallyClosed.
-    + apply t_local_closure_monotonic with (i1 := it); search.
-    + apply IHELocallyClosed.
-      search.
+    apply t_local_closure_monotonic with (i1 := it); search.
   - apply locally_closed_open_for_all; search.
     constructor.
     apply t_local_closure_monotonic with (i1 := nt); search.
diff --git a/proofs_rocq/system_f/preservation.v b/proofs_rocq/system_f/preservation.v
index cd1596de..4d9c5683 100644
--- a/proofs_rocq/system_f/preservation.v
+++ b/proofs_rocq/system_f/preservation.v
@@ -6,7 +6,6 @@
 (**************************************)
 (**************************************)
 
-Require Import Stdlib.Bool.Bool.
 Require Import Stdlib.Lists.List.
 Require Import main.system_f.context.
 Require Import main.system_f.free_var.
diff --git a/proofs_rocq/system_f/typing.v b/proofs_rocq/system_f/typing.v
index ae312931..406387ba 100644
--- a/proofs_rocq/system_f/typing.v
+++ b/proofs_rocq/system_f/typing.v
@@ -6,7 +6,6 @@
 (**************************)
 (**************************)
 
-Require Import Stdlib.Bool.Bool.
 Require Import Stdlib.Lists.List.
 Require Import main.system_f.context.
 Require Import main.system_f.free_var.
diff --git a/proofs_rocq/tactics.v b/proofs_rocq/tactics.v
index 40d10cc3..b3d02948 100644
--- a/proofs_rocq/tactics.v
+++ b/proofs_rocq/tactics.v
@@ -8,9 +8,10 @@
 
 Require Import Stdlib.micromega.Lia.
 
-(* Ensure this hint database exists. *)
+(* Ensure these hint databases exist. *)
 
 Create HintDb main.
+Create Rewrite HintDb main.
 
 (*
   This tactic does a variety of simplifications on the goal and hypotheses.
diff --git a/proofs_rocq/tutorial/lesson3_logic.v b/proofs_rocq/tutorial/lesson3_logic.v
index 6abd3ccd..a5f272a2 100644
--- a/proofs_rocq/tutorial/lesson3_logic.v
+++ b/proofs_rocq/tutorial/lesson3_logic.v
@@ -279,6 +279,13 @@ Inductive eq [A] (x : A) : A -> Prop :=
 Notation "x = y" := (eq x y) : type_scope.
 Notation "x <> y" := (~ (x = y)) : type_scope.
 
+(*
+  The `rewrite` tactic used below requires some machinery to work with our
+  new notion of equality. The following command generates it.
+*)
+
+Scheme Rewriting for eq.
+
 Definition one_plus_one_equals_two : 1 + 1 = 2 := eq_refl 2.
 
 Goal 1 + 1 = 2.
@@ -426,7 +433,8 @@ Definition divisible_by_4_implies_even x :
     | ex_intro y h2 =>
       ex_intro
         (2 * y)
-        match eq_sym (Nat.mul_assoc 2 2 y) in Logic.eq _ z return z = x with
+        match Logic.eq_sym (Nat.mul_assoc 2 2 y) in Logic.eq _ z return z = x
+        with
         | Logic.eq_refl _ => h2
         end
     end.
diff --git a/proofs_rocq/tutorial/lesson4_proof_techniques.v b/proofs_rocq/tutorial/lesson4_proof_techniques.v
index 08d7e938..18789bc3 100644
--- a/proofs_rocq/tutorial/lesson4_proof_techniques.v
+++ b/proofs_rocq/tutorial/lesson4_proof_techniques.v
@@ -6,7 +6,6 @@
 (******************************)
 (******************************)
 
-Require Import Stdlib.Arith.Arith. (* For facts in the `arith` hint database *)
 Require Import Stdlib.micromega.Lia. (* For the `lia` tactic *)
 
 (****************************)
diff --git a/toast.yml b/toast.yml
index e0779990..3f974ed0 100644
--- a/toast.yml
+++ b/toast.yml
@@ -88,12 +88,13 @@ tasks:
     command: |
       # Install Rocq via opam. The `rocq-prover` package is a virtual package
       # with unversioned dependencies on `rocq-core` and `rocq-stdlib`, so
-      # those two packages must be pinned explicitly.
+      # those two packages must be pinned explicitly. Note that `rocq-stdlib`
+      # is versioned independently of `rocq-core`.
       opam init --disable-sandboxing --yes
       eval "$(opam env)"
-      opam pin add --no-action rocq-core 9.0.0 --yes
-      opam pin add --no-action rocq-stdlib 9.0.0 --yes
-      opam pin add rocq-prover 9.0.0 --yes
+      opam pin add --no-action rocq-core 9.2.0 --yes
+      opam pin add --no-action rocq-stdlib 9.1.0 --yes
+      opam pin add --kind version rocq-prover meta.1 --yes
 
   install_tools:
     description: Install the tools needed to verify the Rocq proofs.
@@ -169,10 +170,9 @@ tasks:
         '^\s*Require (Import )?(Stdlib|main)\.' \
         "rocq compile \
           -set 'Default Goal Selector=!' \
-          -set 'Loose Hint Behavior=Strict' \
           -set 'Primitive Projections' \
           -set 'Printing Projections' \
-          -unset 'Printing Primitive Projection Parameters' \
+          -w +default \
           -Q proofs_rocq main ?" \
         $(
           find . -type d \( \
@@ -188,10 +188,9 @@ tasks:
         '^\s*Import ' \
         "rocq compile \
           -set 'Default Goal Selector=!' \
-          -set 'Loose Hint Behavior=Strict' \
           -set 'Primitive Projections' \
           -set 'Printing Projections' \
-          -unset 'Printing Primitive Projection Parameters' \
+          -w +default \
           -Q proofs_rocq main ?" \
         $(
           find . -type d \( \