From 2876f7c688590a64189f47b439f7edf26c91c5de Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 29 Jun 2017 21:32:04 -0400 Subject: Reorganization of saturated arithmetic --- src/Specific/Karatsuba.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'src/Specific/Karatsuba.v') diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v index 2df2df632..97d4149d5 100644 --- a/src/Specific/Karatsuba.v +++ b/src/Specific/Karatsuba.v @@ -1,6 +1,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.Saturated.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable. Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics. @@ -291,8 +292,6 @@ Ltac basesystem_partial_evaluation_RHS := solve_op_F wt x. reflexivity. Defined. - Require Import Crypto.Arithmetic.Saturated. - Section PreFreeze. Lemma wt_pos i : wt i > 0. Proof. -- cgit v1.2.3