From 592b071c48b98a3e0a7fb7a430b5e7650af26004 Mon Sep 17 00:00:00 2001
From: Stephan Boyer <stephan@stephanboyer.com>
Date: Thu, 2 Jul 2026 12:31:42 -0700
Subject: [PATCH 1/4] Update Rocq to 9.2.0

Pin rocq-core 9.2.0 and rocq-stdlib 9.1.0 (the stdlib is now versioned
independently of the prover core). This entails:

- Removing the 'Loose Hint Behavior' flag, which no longer exists.
- Adapting proofs in icbics.v, local_closure.v, and opening.v, where the
  stronger 'search' tactic now closes goals that previously required
  manual steps.
- Importing Stdlib.Vectors.FinFun in icbics.v, where Permutation_nth
  moved.
- Explicitly creating the 'main' hint databases in tactics.v and
  generating the rewriting schemes for the custom equality in
  lesson3_logic.v, as implicit creation is deprecated since 9.2. The
  implicit-creation warnings are escalated to errors so that
  lint-imports recognizes hint-database dependencies.
- Removing imports that are no longer needed with the new stdlib.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 _RocqProject                                    |  2 +-
 proofs_rocq/category_theory/arrow.v             |  2 --
 proofs_rocq/category_theory/coproduct.v         |  1 -
 proofs_rocq/category_theory/object.v            |  1 -
 proofs_rocq/category_theory/terminal.v          |  1 -
 proofs_rocq/icbics/icbics.v                     |  7 +------
 proofs_rocq/kleene/kleene_data.v                |  2 ++
 proofs_rocq/stlc/name.v                         |  1 -
 proofs_rocq/system_f/context.v                  |  1 -
 proofs_rocq/system_f/local_closure.v            |  3 ---
 proofs_rocq/system_f/name.v                     |  1 -
 proofs_rocq/system_f/opening.v                  |  9 ++-------
 proofs_rocq/system_f/preservation.v             |  1 -
 proofs_rocq/system_f/typing.v                   |  1 -
 proofs_rocq/tactics.v                           |  3 ++-
 proofs_rocq/tutorial/lesson3_logic.v            | 10 +++++++++-
 proofs_rocq/tutorial/lesson4_proof_techniques.v |  1 -
 toast.yml                                       | 13 +++++++------
 18 files changed, 24 insertions(+), 36 deletions(-)

diff --git a/_RocqProject b/_RocqProject
index b85bd434..e58454b3 100644
--- a/_RocqProject
+++ b/_RocqProject
@@ -1,7 +1,7 @@
 # [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 +implicit-create-hint-db,+implicit-create-rewrite-hint-db"
 -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..a1980af8 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 rocq-prover meta.1 --yes
 
   install_tools:
     description: Install the tools needed to verify the Rocq proofs.
@@ -169,10 +170,10 @@ 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 +implicit-create-hint-db,+implicit-create-rewrite-hint-db \
           -Q proofs_rocq main ?" \
         $(
           find . -type d \( \
@@ -188,10 +189,10 @@ 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 +implicit-create-hint-db,+implicit-create-rewrite-hint-db \
           -Q proofs_rocq main ?" \
         $(
           find . -type d \( \

From 1b033d22b0fca7b4e87f7607928f8462a3b41235 Mon Sep 17 00:00:00 2001
From: Stephan Boyer <stephan@stephanboyer.com>
Date: Thu, 2 Jul 2026 12:41:02 -0700
Subject: [PATCH 2/4] Specify the pin kind explicitly for rocq-prover

Unlike "9.0.0", opam doesn't recognize "meta.1" as a version, so
without an explicit kind it interprets the pin target as a path.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 toast.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toast.yml b/toast.yml
index a1980af8..39066542 100644
--- a/toast.yml
+++ b/toast.yml
@@ -94,7 +94,7 @@ tasks:
       eval "$(opam env)"
       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 rocq-prover meta.1 --yes
+      opam pin add --kind version rocq-prover meta.1 --yes
 
   install_tools:
     description: Install the tools needed to verify the Rocq proofs.

From 6fcbd713d23017d44869c05aeda24cc6300e7802 Mon Sep 17 00:00:00 2001
From: Stephan Boyer <stephan@stephanboyer.com>
Date: Thu, 2 Jul 2026 13:15:14 -0700
Subject: [PATCH 3/4] Escalate all default-enabled warnings to errors

The build is warning-free, so this enforces that it stays that way.
This subsumes the implicit-create-hint-db escalations and also turns
unknown options, deprecated definitions, etc. into hard errors.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 _RocqProject | 2 +-
 toast.yml    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/_RocqProject b/_RocqProject
index e58454b3..ed3fb6bd 100644
--- a/_RocqProject
+++ b/_RocqProject
@@ -3,5 +3,5 @@
 -arg "-set 'Primitive Projections'"
 -arg "-set 'Printing Projections'"
 -arg "-unset 'Printing Primitive Projection Parameters'"
--arg "-w +implicit-create-hint-db,+implicit-create-rewrite-hint-db"
+-arg "-w +default"
 -Q proofs_rocq main
diff --git a/toast.yml b/toast.yml
index 39066542..55001698 100644
--- a/toast.yml
+++ b/toast.yml
@@ -173,7 +173,7 @@ tasks:
           -set 'Primitive Projections' \
           -set 'Printing Projections' \
           -unset 'Printing Primitive Projection Parameters' \
-          -w +implicit-create-hint-db,+implicit-create-rewrite-hint-db \
+          -w +default \
           -Q proofs_rocq main ?" \
         $(
           find . -type d \( \
@@ -192,7 +192,7 @@ tasks:
           -set 'Primitive Projections' \
           -set 'Printing Projections' \
           -unset 'Printing Primitive Projection Parameters' \
-          -w +implicit-create-hint-db,+implicit-create-rewrite-hint-db \
+          -w +default \
           -Q proofs_rocq main ?" \
         $(
           find . -type d \( \

From 84cab0fec92e4fda5044f581829544414a878673 Mon Sep 17 00:00:00 2001
From: Stephan Boyer <stephan@stephanboyer.com>
Date: Thu, 2 Jul 2026 13:20:32 -0700
Subject: [PATCH 4/4] Remove a flag which matches the default behavior

'Printing Primitive Projection Parameters' is off by default.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 _RocqProject | 1 -
 toast.yml    | 2 --
 2 files changed, 3 deletions(-)

diff --git a/_RocqProject b/_RocqProject
index ed3fb6bd..cd5d98f7 100644
--- a/_RocqProject
+++ b/_RocqProject
@@ -2,6 +2,5 @@
 -arg "-set 'Default Goal Selector=!'"
 -arg "-set 'Primitive Projections'"
 -arg "-set 'Printing Projections'"
--arg "-unset 'Printing Primitive Projection Parameters'"
 -arg "-w +default"
 -Q proofs_rocq main
diff --git a/toast.yml b/toast.yml
index 55001698..3f974ed0 100644
--- a/toast.yml
+++ b/toast.yml
@@ -172,7 +172,6 @@ tasks:
           -set 'Default Goal Selector=!' \
           -set 'Primitive Projections' \
           -set 'Printing Projections' \
-          -unset 'Printing Primitive Projection Parameters' \
           -w +default \
           -Q proofs_rocq main ?" \
         $(
@@ -191,7 +190,6 @@ tasks:
           -set 'Default Goal Selector=!' \
           -set 'Primitive Projections' \
           -set 'Printing Projections' \
-          -unset 'Printing Primitive Projection Parameters' \
           -w +default \
           -Q proofs_rocq main ?" \
         $(