diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
| commit | c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch) | |
| tree | db7187f6984acff324ca468e7b33d9285806a1eb /src/Util/AdditionChainExponentiation.v | |
| parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) | |
rename-everything
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. |