Merge pull request #45 from tabareau/sortpoly-equality

add overlay (backward compat)

Author: samuelgruetter

Kami/Ex/Divider32.v

@@ -182,15 +182,15 @@ 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
       | [ |- existT _ (n + ?mn) _ = _ ] =>
         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

Kami/Ex/Divider64.v

@@ -182,15 +182,15 @@ 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
       | [ |- existT _ (n + ?mn) _ = _ ] =>
         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

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.

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.