diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-10 18:07:11 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-10 18:07:11 -0400 |
| commit | 7a163ef981507f254dd6b5d343acdedc331274c7 (patch) | |
| tree | c15240923a6cb365ca1b2b6120792b618f56810d /src/CompleteEdwardsCurve/Pre.v | |
| parent | 7129157393f420268c9399dc9b4119469994bf63 (diff) | |
Minor 8.5 changes
Diffstat (limited to 'src/CompleteEdwardsCurve/Pre.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 322db1792..f10e587d6 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -144,7 +144,7 @@ Section Pre. (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1; * c=1 and an extra a in front of x^2 *) - injection H; clear H; intros. + injection H; cbv beta iota; clear H; intros. Ltac t x1 y1 x2 y2 := assert ((a*x2^2 + y2^2)*d*x1^2*y1^2 |