From 6441681c8b861250ab12eb22e8458dff59f84ea3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 27 Oct 2016 14:26:56 -0400 Subject: Fix a missing import in previous commit --- src/ModularArithmetic/ModularBaseSystem.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 615bd832b..d8303d1a7 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -7,6 +7,7 @@ Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.ModularArithmetic.ModularBaseSystemList. Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. -- cgit v1.2.3