diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-22 16:09:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-22 16:09:02 -0400 |
| commit | 28508c6fa3ee811d8e51f365cd6cbdabe96352cd (patch) | |
| tree | 5aa261e20ea677cb9ad50907d7a84588a296a013 /src/Arithmetic/CoreUnfolder.v | |
| parent | 91c0f39a5c7236489e268de0e5fa97b055698e4c (diff) | |
Add another unfolding database
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 |