diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-21 17:34:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-21 17:34:22 -0400 |
| commit | 0709bc79077cf52682d01ce432b0f35c6f27665e (patch) | |
| tree | 7de531290887cba3bfd94cb107f72b04483faebd /src/Specific/GF25519.v | |
| parent | acd8180a1626ca35c19de7d797dd80e1e22f5799 (diff) | |
pow, not pow_opt, in Specific/GF25519
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 42797c1a1..1ded72383 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -577,6 +577,7 @@ Definition sqrt_sig (f : fe25519) : Proof. eexists. cbv [sqrt_5mod8_opt]. + rewrite <- pow_correct. apply Proper_Let_In_nd_changebody; [reflexivity|intro]. set_evars. rewrite <-!mul_correct, <-eqb_correct. subst_evars. reflexivity. |