diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-14 23:54:12 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-15 00:12:44 -0400 |
| commit | fe63118de92560724d27c5e3f3ad84a5b210cdfc (patch) | |
| tree | a8cd81f28b6064fa8dae07a427d381921182539e /src/Compilers/LinearizeInterp.v | |
| parent | 2d163540e9ce4dada64a496452eed910d7a4ec91 (diff) | |
Add a bit more power to side conditions in reflective_interp rewrite db
Diffstat (limited to 'src/Compilers/LinearizeInterp.v')
| -rw-r--r-- | src/Compilers/LinearizeInterp.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Compilers/LinearizeInterp.v b/src/Compilers/LinearizeInterp.v index 4c8347987..c5fafef45 100644 --- a/src/Compilers/LinearizeInterp.v +++ b/src/Compilers/LinearizeInterp.v @@ -1,5 +1,6 @@ (** * Linearize: Place all and only operations in let binders *) Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. Require Import Crypto.Compilers.Relations. Require Import Crypto.Compilers.InterpProofs. Require Import Crypto.Compilers.Linearize. @@ -122,4 +123,4 @@ Section language. End language. Hint Rewrite @interpf_under_letsf : reflective_interp. -Hint Rewrite @InterpLinearize_gen @interp_linearize_gen @interpf_linearizef_gen @InterpLinearize @interp_linearize @interpf_linearizef @InterpANormal @interp_a_normal @interpf_a_normalf using solve [ eassumption | eauto with wf ] : reflective_interp. +Hint Rewrite @InterpLinearize_gen @interp_linearize_gen @interpf_linearizef_gen @InterpLinearize @interp_linearize @interpf_linearizef @InterpANormal @interp_a_normal @interpf_a_normalf using solve_wf_side_condition : reflective_interp. |