From c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 6 Apr 2017 22:53:07 -0400 Subject: rename-everything --- src/Util/AdditionChainExponentiation.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/AdditionChainExponentiation.v') 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. -- cgit v1.2.3