From 5e985612bd0daad83f61040b9bbde4cd9ced4974 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 28 Oct 2025 16:16:13 +0100
Subject: [PATCH] Adapt to rocq-prover/rocq#21241 (stop relying on eq_rec being
 defined from eq_rect)

---
 src/bbv/DepEq.v |  3 ++-
 src/bbv/Word.v  | 14 +++++++-------
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/bbv/DepEq.v b/src/bbv/DepEq.v
index 560b3f1..49beb5e 100644
--- a/src/bbv/DepEq.v
+++ b/src/bbv/DepEq.v
@@ -24,7 +24,8 @@ Ltac generalize_proof :=
     end.
 
 Ltac eq_rect_simpl :=
-  unfold eq_rec_r, eq_rec;
+  unfold eq_rec_r;
+  change eq_rec with (fun A x (P:A -> Set) => @eq_rect A x P);
   repeat rewrite eq_rect_nat_double;
   repeat rewrite <- (eq_rect_eq_dec eq_nat_dec).
 
diff --git a/src/bbv/Word.v b/src/bbv/Word.v
index 9becfb7..2122a23 100644
--- a/src/bbv/Word.v
+++ b/src/bbv/Word.v
@@ -4022,7 +4022,7 @@ Lemma wrshifta_0:
   forall sz (w: word sz), wrshifta w 0 = w.
 Proof.
   unfold wrshifta; intros; simpl.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   unfold sext.
   destruct (wmsb w false).
   - cbn; rewrite combine_n_0.
@@ -4035,7 +4035,7 @@ Lemma wrshifta_WO:
   forall n, wrshifta WO n = WO.
 Proof.
   unfold wrshifta; cbn; intros.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite wzero_eq_rect.
   rewrite <-combine_wzero.
   rewrite split2_combine.
@@ -4062,7 +4062,7 @@ Proof.
   intros.
   unfold wrshifta; cbn.
   rewrite sext_wzero.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite wzero_eq_rect.
   rewrite <-combine_wzero.
   rewrite split2_combine.
@@ -4346,7 +4346,7 @@ Lemma wordToNat_wrshifta:
 Proof.
   unfold wrshifta; intros.
   rewrite wordToNat_split2.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite wordToNat_eq_rect.
   reflexivity.
 Qed.
@@ -4383,7 +4383,7 @@ Proof.
 
   - unfold wlshift; intros.
     rewrite wordToNat_split1.
-    unfold eq_rec_r, eq_rec.
+    eq_rect_simpl.
     rewrite wordToNat_eq_rect.
     rewrite wordToNat_combine.
     rewrite wordToNat_wzero; simpl.
@@ -6977,7 +6977,7 @@ Proof.
   apply wordToNat_inj.
   unfold wlshift.
   rewrite? wordToNat_split1.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite? wordToNat_eq_rect.
   rewrite? wordToNat_combine.
   rewrite? wordToNat_wzero.
@@ -7038,7 +7038,7 @@ Proof.
   apply wordToNat_inj.
   unfold wlshift.
   rewrite? wordToNat_split1.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite? wordToNat_eq_rect.
   rewrite? wordToNat_combine.
   rewrite? wordToNat_wzero.