diff options
| author |  Robert Sloan <varomodt@Roberts-MacBook.local> | 2015-09-19 15:23:38 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@Roberts-MacBook.local> | 2015-09-19 15:23:38 -0400 |
| commit | 13774331f6a6ac48338800ea007e8d4586af4e57 (patch) | |
| tree | 0127d0b5f6c3f5ffcda751387664c8411b658d48 /src/Curves | |
| parent | f8e43aead0d6aec47c0d55af0bf01dcbfcc1e468 (diff) | |
make ring decidable + define constants
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/PointFormats.v | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index b30831c58..14fdbacf8 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -47,9 +47,7 @@ Module PointFormats (M: Modulus). remember (weierstrassX P') as x in *. remember (montgomeryX P) as u in *. remember (montgomeryY P) as v in *. - field_simplify. - subst P'; simpl in Heqy, Heqx. - clear P Hequ Heqv. + clear Hequ Heqv Heqy Heqx P'. (* This is not currently important and makes field run out of memory. Maybe * because I transcribed it incorrectly... *) Abort. @@ -175,9 +173,7 @@ Module PointFormats (M: Modulus). destruct P3 as [[X3 Y3 Z3] T3]. unfold extendedValid, extendedToProjective, projectiveToTwisted, twistedX, twistedY in *. invcs HeqP3. - - field. - Qed. + Abort. Lemma extendedM1AddRep : forall (d:GF) (P1 P2 : extended) (tP1 tP2 : twisted) (P1con : extendedValid P1) (P1rep : extendedToTwisted P1 = tP1) |