diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v index 154a3d29e..cee5718d3 100644 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v @@ -6,7 +6,8 @@ Require Import Crypto.Compilers.Z.MapCastByDeBruijnWf. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Syntax.Util. Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas. +Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.IsBoundedBy. +Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.PullCast. Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. Definition Wf_MapCast |