From e8fab6b839e19da231333ca8173bbb2a3d8a4033 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 11 Feb 2017 21:59:58 -0500 Subject: split the algebra library; use fsatz more --- src/Util/AdditionChainExponentiation.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/AdditionChainExponentiation.v') diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index cf8a68340..97c3e02a3 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -1,7 +1,7 @@ Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations. Require Import Coq.Numbers.BinNums Coq.NArith.BinNat. Require Import Crypto.Util.ListUtil. -Require Import Crypto.Algebra. Import Monoid ScalarMult. +Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.Option. -- cgit v1.2.3