diff options
Diffstat (limited to 'src/Util/AdditionChainExponentiation.v')
| -rw-r--r-- | src/Util/AdditionChainExponentiation.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index 110a756ea..e03b2e36f 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 Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. +Require Import Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. Require Import Crypto.Util.Option. Require Import Crypto.Util.Tactics.BreakMatch. @@ -28,7 +28,7 @@ Section AddChainExp. (0, 6)] (* 31 = 30 + 1 *) [1] = 31. reflexivity. Qed. - Context {G eq op id} {monoid:@Algebra.monoid G eq op id}. + Context {G eq op id} {monoid:@Algebra.Hierarchy.monoid G eq op id}. Context {scalarmult} {is_scalarmult:@ScalarMult.is_scalarmult G eq op id scalarmult}. Local Infix "=" := eq : type_scope. Local Open Scope N_scope. |