From 3e1d1319b85ca84a2f34c86ea7fa83f174a948a1 Mon Sep 17 00:00:00 2001
From: nicolas tabareau <nicolas.tabareau@gmail.com>
Date: Wed, 19 Nov 2025 08:57:47 +0100
Subject: [PATCH] add overlay (backward compat)

---
 Kami/Ex/Divider32.v    |  4 ++--
 Kami/Ex/Divider64.v    |  4 ++--
 Kami/Ex/Multiplier32.v | 12 ++++++------
 Kami/Ex/Multiplier64.v | 10 +++++-----
 4 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Kami/Ex/Divider32.v b/Kami/Ex/Divider32.v
index 8a00f95..ee621ae 100644
--- a/Kami/Ex/Divider32.v
+++ b/Kami/Ex/Divider32.v
@@ -182,7 +182,7 @@ Section Divider32.
     cbv [evalZeroExtendTrunc evalSignExtendTrunc].
     destruct (lt_dec _ _); [|lia].
     apply existT_wminus.
-    - unfold zext, eq_rec.
+    - unfold zext. eq_rect_simpl.
       change (fun n2 => word n2) with word.
       rewrite existT_eq_rect.
       match goal with
@@ -190,7 +190,7 @@ Section Divider32.
         replace mn with 1 by (clear; induction n; auto)
       end.
       reflexivity.
-    - unfold zext, eq_rec.
+    - unfold zext. eq_rect_simpl.
       change (fun n2 => word n2) with word.
       rewrite existT_eq_rect.
       match goal with
diff --git a/Kami/Ex/Divider64.v b/Kami/Ex/Divider64.v
index 13d15eb..4493848 100644
--- a/Kami/Ex/Divider64.v
+++ b/Kami/Ex/Divider64.v
@@ -182,7 +182,7 @@ Section Divider64.
     cbv [evalZeroExtendTrunc].
     destruct (lt_dec _ _); [|lia].
     apply existT_wminus.
-    - unfold zext, eq_rec.
+    - unfold zext. eq_rect_simpl.
       change (fun n2 => word n2) with word.
       rewrite existT_eq_rect.
       match goal with
@@ -190,7 +190,7 @@ Section Divider64.
         replace mn with 1 by (clear; induction n; auto)
       end.
       reflexivity.
-    - unfold zext, eq_rec.
+    - unfold zext. eq_rect_simpl.
       change (fun n2 => word n2) with word.
       rewrite existT_eq_rect.
       match goal with
diff --git a/Kami/Ex/Multiplier32.v b/Kami/Ex/Multiplier32.v
index dcf1233..7ca25c0 100644
--- a/Kami/Ex/Multiplier32.v
+++ b/Kami/Ex/Multiplier32.v
@@ -1198,9 +1198,9 @@ Section Multiplier32.
         kinv_custom boothMultiplierInv_old.
         boothMultiplierInv_new.
         
-        * cbn; unfold eq_rec; eq_rect_simpl.
+        * cbn. eq_rect_simpl.
           reflexivity.
-        * cbn; unfold eq_rec; eq_rect_simpl.
+        * cbn; eq_rect_simpl.
           reflexivity.
         * clear -H4 H12.
           Opaque split2.
@@ -1214,7 +1214,7 @@ Section Multiplier32.
           find_if_inside; [discriminate|].
           elim n; assumption.
 
-        * simpl; unfold eq_rec; eq_rect_simpl.
+        * simpl; eq_rect_simpl.
 
           assert (Hx1: x Fin.F1 <> wpow2 MultNumBits).
           { intro Hx.
@@ -1247,7 +1247,7 @@ Section Multiplier32.
           repeat split.
           { subst ww.
             cbv [evalSignExtendTrunc].
-            simpl; unfold eq_rec; eq_rect_simpl.
+            simpl; eq_rect_simpl.
             rewrite <-H13.
             reflexivity.
           }
@@ -1386,7 +1386,7 @@ Section Multiplier32.
         unfold wmultZ, wordBinZ.
         pose proof (sext_wordToZ 33 bsiM).
         cbv [evalSignExtendTrunc]; cbn.
-        unfold eq_rec; eq_rect_simpl.
+        eq_rect_simpl.
         cbn in H1; rewrite H1.
         pose proof (sext_wordToZ 33 bsiR).
         cbn; cbn in H2; rewrite H2.
@@ -1408,7 +1408,7 @@ Section Multiplier32.
         unfold wmultZ, wordBinZ.
         pose proof (sext_wordToZ 33 bsiM).
         cbv [evalSignExtendTrunc]; cbn.
-        unfold eq_rec; eq_rect_simpl.
+        eq_rect_simpl.
         cbn in H1; rewrite H1.
         pose proof (sext_wordToZ 33 bsiR).
         cbn; cbn in H2; rewrite H2.
diff --git a/Kami/Ex/Multiplier64.v b/Kami/Ex/Multiplier64.v
index f8412cd..6bf370d 100644
--- a/Kami/Ex/Multiplier64.v
+++ b/Kami/Ex/Multiplier64.v
@@ -1198,9 +1198,9 @@ Section Multiplier64.
         kinv_custom boothMultiplierInv_old.
         boothMultiplierInv_new.
         
-        * cbn; unfold eq_rec; eq_rect_simpl.
+        * cbn; eq_rect_simpl.
           reflexivity.
-        * cbn; unfold eq_rec; eq_rect_simpl.
+        * cbn; eq_rect_simpl.
           reflexivity.
         * clear -H4 H12.
           Opaque split2.
@@ -1247,7 +1247,7 @@ Section Multiplier64.
           repeat split.
           { subst ww.
             cbv [evalSignExtendTrunc].
-            simpl; unfold eq_rec; eq_rect_simpl.
+            simpl; eq_rect_simpl.
             rewrite <-H13.
             reflexivity.
           }
@@ -1386,7 +1386,7 @@ Section Multiplier64.
         unfold wmultZ, wordBinZ.
         pose proof (sext_wordToZ 65 bsiM).
         cbv [evalSignExtendTrunc]; cbn.
-        unfold eq_rec; eq_rect_simpl.
+        eq_rect_simpl.
         cbn in H1; rewrite H1.
         pose proof (sext_wordToZ 65 bsiR).
         cbn; cbn in H2; rewrite H2.
@@ -1408,7 +1408,7 @@ Section Multiplier64.
         unfold wmultZ, wordBinZ.
         pose proof (sext_wordToZ 65 bsiM).
         cbv [evalSignExtendTrunc]; cbn.
-        unfold eq_rec; eq_rect_simpl.
+        eq_rect_simpl.
         cbn in H1; rewrite H1.
         pose proof (sext_wordToZ 65 bsiR).
         cbn; cbn in H2; rewrite H2.