diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-29 21:32:04 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-29 21:32:04 -0400 |
| commit | 2876f7c688590a64189f47b439f7edf26c91c5de (patch) | |
| tree | fffe55bc24e83105fca356a81a352e1fa4309999 /src/Specific/ArithmeticSynthesisTest.v | |
| parent | b291707642db5986240b3e9eb9a80839d81ffe42 (diff) | |
Reorganization of saturated arithmetic
Diffstat (limited to 'src/Specific/ArithmeticSynthesisTest.v')
| -rw-r--r-- | src/Specific/ArithmeticSynthesisTest.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v index 0ea85e866..a2e1442a4 100644 --- a/src/Specific/ArithmeticSynthesisTest.v +++ b/src/Specific/ArithmeticSynthesisTest.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. Require Import Coq.Lists.List. Import ListNotations. Require Import Crypto.Arithmetic.Core. Import B. Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Arithmetic.Saturated.Freeze. Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable. Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics. Require Crypto.Util.Tuple. @@ -232,8 +233,6 @@ Section Ops51. solve_op_F wt x. reflexivity. Defined. - Require Import Crypto.Arithmetic.Saturated. - Section PreFreeze. Lemma wt_pos i : wt i > 0. Proof. |