Add another unfolding database

4 files changed, 12 insertions, 2 deletions

diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index 5104a21aa..4df36a0aa 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -1133,7 +1133,7 @@ Ltac pattern_strip_full t :=
   let t := (eval pattern
                  (@Let_In Z (fun _ => Z)),
             @Z.add_get_carry_cps, @Z.mul_split_at_bitwidth_cps,
-            Z.eq_dec_cps, Z.eqb_cps,
+            (@Z.eq_dec_cps), (@Z.eqb_cps),
             @runtime_mul, @runtime_add, @runtime_opp, @runtime_shr, @runtime_and, @runtime_lor,
             (@id_with_alt Z),
             @Z.add_get_carry, @Z.zselect, @Z.mul_split_at_bitwidth,
@@ -1165,7 +1165,7 @@ Ltac apply_patterned_full t1 :=
             (@Let_In) (@id_with_alt)
             (@Let_In Z (fun _ => Z))
             (@Z.add_get_carry_cps) (@Z.mul_split_at_bitwidth_cps)
-            Z.eq_dec_cps Z.eqb_cps
+            (@Z.eq_dec_cps) (@Z.eqb_cps)
             (@runtime_mul) (@runtime_add) (@runtime_opp) (@runtime_shr) (@runtime_and) (@runtime_lor)
             (@id_with_alt Z)
             (@Z.add_get_carry) (@Z.zselect) (@Z.mul_split_at_bitwidth)
diff --git a/src/Arithmetic/CoreUnfolder.v b/src/Arithmetic/CoreUnfolder.v
index 05aa2f498..a7a7286d1 100644
--- a/src/Arithmetic/CoreUnfolder.v
+++ b/src/Arithmetic/CoreUnfolder.v
@@ -1,9 +1,15 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.CPS.
 Require Import Crypto.Util.IdfunWithAlt.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.Tactics.VM.
 
+Create HintDb arithmetic_cps_unfolder.
+
+Hint Unfold Core.div Core.modulo : arithmetic_cps_unfolder.
+
 Ltac make_parameterized_sig t :=
   refine (_ : { v : _ | v = t });
   eexists; cbv delta [t
diff --git a/src/Arithmetic/Saturated/CoreUnfolder.v b/src/Arithmetic/Saturated/CoreUnfolder.v
index 2b2b2ed09..9a0e0c06a 100644
--- a/src/Arithmetic/Saturated/CoreUnfolder.v
+++ b/src/Arithmetic/Saturated/CoreUnfolder.v
@@ -1,6 +1,8 @@
 Require Import Crypto.Arithmetic.CoreUnfolder.
 Require Import Crypto.Arithmetic.Saturated.Core.
 
+Hint Unfold Core.Columns.compact_digit_cps Core.Columns.compact_step_cps Core.Columns.compact_cps : arithmetic_cps_unfolder.
+
 Module Columns.
   (**
 <<
diff --git a/src/Arithmetic/Saturated/WrappersUnfolder.v b/src/Arithmetic/Saturated/WrappersUnfolder.v
index d28719af8..b8fe6afc6 100644
--- a/src/Arithmetic/Saturated/WrappersUnfolder.v
+++ b/src/Arithmetic/Saturated/WrappersUnfolder.v
@@ -3,6 +3,8 @@ Require Import Crypto.Arithmetic.Saturated.CoreUnfolder.
 Require Import Crypto.Arithmetic.Saturated.MulSplitUnfolder.
 Require Import Crypto.Arithmetic.Saturated.Wrappers.
 
+Hint Unfold Wrappers.Columns.add_cps Wrappers.Columns.unbalanced_sub_cps Wrappers.Columns.mul_cps : arithmetic_cps_unfolder.
+
 Module Columns.
   (**
 <<