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 | |
| parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) | |
rename-everything
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/AdditionChainExponentiation.v | 4 | ||||
| -rw-r--r-- | src/Util/IterAssocOp.v | 8 |
2 files changed, 6 insertions, 6 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. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 2fd7f8adc..e4f9dde08 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -1,7 +1,7 @@ Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. +Require Import Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. Require Import Crypto.Util.NUtil. Require Import Crypto.Util.Tactics.BreakMatch. @@ -9,7 +9,7 @@ Local Open Scope equiv_scope. Generalizable All Variables. Section IterAssocOp. - Context {T eq op id} {moinoid : @monoid T eq op id} (testbit : nat -> bool). + Context {T eq op id} {moinoid : @Algebra.Hierarchy.monoid T eq op id} (testbit : nat -> bool). Local Infix "===" := eq. Local Infix "===" := eq : type_scope. Local Notation nat_iter_op := (ScalarMult.scalarmult_ref (add:=op) (zero:=id)). @@ -26,12 +26,12 @@ Section IterAssocOp. Lemma Pos_iter_op_succ : forall p a, Pos.iter_op op (Pos.succ p) a === op a (Pos.iter_op op p a). Proof using Type*. - induction p; intros; simpl; rewrite ?associative, ?IHp; reflexivity. + induction p; intros; simpl; rewrite ?Algebra.Hierarchy.associative, ?IHp; reflexivity. Qed. Lemma N_iter_op_succ : forall n a, N_iter_op (N.succ n) a === op a (N_iter_op n a). Proof using Type*. - destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?right_identity; reflexivity. + destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?Algebra.Hierarchy.right_identity; reflexivity. Qed. Lemma N_iter_op_is_nat_iter_op : forall n a, N_iter_op n a === nat_iter_op (N.to_nat n) a. |