fix the makefile to not rebuild + module renaming

2 files changed, 11 insertions, 22 deletions

diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index fc6cbb104..fc40d9136 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -1,39 +1,29 @@
 Require Import Zpower ZArith Znumtheory.
-Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory.
+Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
 Require Import Crypto.Curves.PointFormats.
 
-Definition two_255_19 := (two_p 255) - 19.
-Lemma two_255_19_prime : prime two_255_19.
-  (* <http://safecurves.cr.yp.to/proof/57896044618658097711785492504343953926634992332820282019728792003956564819949.html>,
-  * <https://github.com/sipa/Coin25519/blob/master/spec/primeCerts/prime57896044618658097711785492504343953926634992332820282019728792003956564819949.v#L16> *)
-Admitted.
-
-Definition prime25519 := exist _ two_255_19 two_255_19_prime.
-Local Notation p := two_255_19.
-
-Module Modulus25519 <: Modulus.
-  Definition modulus := prime25519.
-End Modulus25519.
-
 Module Curve25519.
-  Module PointFormats25519 := PointFormats Modulus25519.
-  Import Modulus25519 PointFormats25519 PointFormats25519.Theory PointFormats25519.Field.
+  Module PF := PointFormats.
+  Import PF.
   Local Open Scope GF_scope.
 
   Definition A : GF := ZToGF 486662.
   Definition d : GF := ((0 -ZToGF 121665) / (ZToGF 121666))%GF.
 
-
   Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A.
+
+  (* Module-izing Twisted was a breaking change
   Definition m1TwistedOnCurve25519 := twistedOnCurve (0 -1) d.
 
   Definition identityTwisted : twisted := mkTwisted 0 1.
 
   Lemma identityTwistedOnCurve : m1TwistedOnCurve25519 identityTwisted.
-    unfold m1TwistedOnCurve25519, twistedOnCurve, identityTwisted.
+    unfold m1TwistedOnCurve25519, twistedOnCurve.
     simpl; field.
   Qed.
 
+  *)
+
   Definition basepointY := ZToGF 4 / ZToGF 5.
   (* TODO(andreser): implement (in PointFormats) recoverX from <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
 End Curve25519.
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index a72d5d5e0..3962e1d90 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -1,5 +1,5 @@
 
-Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory.
+Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
 Require Import Tactics.VerdiTactics.
 
 (* FIXME: remove after [field] with modulus as a parameter (34d9f8a6e6a4be439d1c56a8b999d2c21ee12a46) is fixed *)
@@ -15,9 +15,8 @@ End M.
 (** Theory of elliptic curves over prime fields for cryptographic applications,
 with focus on the curves in <https://tools.ietf.org/html/draft-ladd-safecurves-04> *)
 Module PointFormats.
-  Module Field := GaloisField M.
-  Module Theory := GaloisFieldTheory M.
-  Import M Field Theory.
+  Module F := ComputationalGaloisField M.
+  Export M F F.T.
   Local Open Scope GF_scope.
   Local Notation "2" := (1+1).
   Local Notation "3" := (1+1+1).