diff options
Diffstat (limited to 'src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v')
| -rw-r--r-- | src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v index c2b87d5a4..672a62685 100644 --- a/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v +++ b/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v @@ -5,7 +5,8 @@ Require Import Crypto.BoundedArithmetic.Double.Core. Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SimplifyProjections. Require Import Crypto.Util.Notations. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Prod. |