diff options
Diffstat (limited to 'src/Arithmetic/CoreUnfolder.v')
| -rw-r--r-- | src/Arithmetic/CoreUnfolder.v | 6 |
1 files changed, 6 insertions, 0 deletions
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 |