aboutsummaryrefslogtreecommitdiff
path: root/src/AbstractInterpretationZRangeProofs.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-04-02 17:51:17 -0400
committerGravatar Jason Gross <jgross@mit.edu>2019-04-02 17:51:17 -0400
commitef3ce824f87fd11eed78a13a884579499a8ffc53 (patch)
treea6af1f34cffc7dedee718e263f6e5d2751eaf28c /src/AbstractInterpretationZRangeProofs.v
parentbacfa270c0c492ef8518d360d87e46cee292474f (diff)
Add Z.combine_at_bitwidth
Diffstat (limited to 'src/AbstractInterpretationZRangeProofs.v')
-rw-r--r--src/AbstractInterpretationZRangeProofs.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/AbstractInterpretationZRangeProofs.v b/src/AbstractInterpretationZRangeProofs.v
index 2ca2ea140..7fb9f4072 100644
--- a/src/AbstractInterpretationZRangeProofs.v
+++ b/src/AbstractInterpretationZRangeProofs.v
@@ -22,6 +22,7 @@ Require Import Crypto.Util.ZUtil.CC.
Require Import Crypto.Util.ZUtil.MulSplit.
Require Import Crypto.Util.ZUtil.Rshi.
Require Import Crypto.Util.ZUtil.Zselect.
+Require Import Crypto.Util.ZUtil.Combine.
Require Import Crypto.Util.ZUtil.Le.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.