diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-06-14 00:36:23 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-06-14 13:05:52 -0400 |
| commit | 53d6e0a991ce110864b2293eb25feca4042186eb (patch) | |
| tree | 5a63e122cd2444aa12531f5f7a3bef159c7cca69 /src/Curves | |
| parent | 362eaa5da1f291b86aa04e8d745738a647ee34ce (diff) | |
ScalarMult: Z -> G -> G (closes #193)
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Edwards/AffineProofs.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v index 8e69b78fe..ec67c25b2 100644 --- a/src/Curves/Edwards/AffineProofs.v +++ b/src/Curves/Edwards/AffineProofs.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra.Hierarchy Crypto.Util.Decidable. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult Crypto.Util.Decidable. Require Import Coq.Logic.Eqdep_dec. Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relation_Definitions. @@ -12,7 +12,7 @@ Require Import Crypto.Util.Tactics.SetoidSubst. Require Export Crypto.Util.FixCoqMistakes. Module E. - Import Group ScalarMult Ring Field CompleteEdwardsCurve.E. + Import Group Ring Field CompleteEdwardsCurve.E. Notation onCurve_zero := Pre.onCurve_zero. Notation denominator_nonzero := Pre.denominator_nonzero. @@ -91,9 +91,6 @@ Module E. induction n; (reflexivity || eapply (_:Proper (eq==>eq==>eq) add); eauto). Qed. - Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul. - Proof using Type. split; intros; (reflexivity || exact _). Qed. - Section PointCompression. Local Notation "x ^ 2" := (x*x). |