diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-10 14:09:59 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-10 14:10:34 -0500 |
| commit | 497ac4e2e7e331c48eddfd428f2287c5384c9c08 (patch) | |
| tree | 10e783e653abc182a5767c1082ccd6a6f57900d0 /src/Experiments | |
| parent | 3552e1b50b6f96f02610795665db8401a4d58c8d (diff) | |
Work around looping in 8.4
This fixes #96
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 20208924d..d3b9c4af6 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -1354,7 +1354,8 @@ Proof. rewrite ModularBaseSystemProofs.encode_rep. symmetry. eapply @ModularBaseSystemProofs.sqrt_5mod8_correct; - eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; + [ eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze.. + | | | ]; prove_bounded_by; match goal with | |- appcontext[GF25519Bounded.powW ?a ?ch] => @@ -1510,7 +1511,7 @@ Section X25519Constants. (a24). Proof. vm_decide_no_check. Qed. End X25519Constants. - + Definition x25519 (n:N) (x:GF25519BoundedCommon.fe25519) : GF25519BoundedCommon.fe25519 := @MxDH.montladder GF25519BoundedCommon.fe25519 GF25519BoundedCommon.zero GF25519BoundedCommon.one GF25519Bounded.add GF25519Bounded.sub @@ -1536,4 +1537,4 @@ Definition x25519_correct' n x : Print Assumptions x25519_correct'. Let three_correct := (@sign_correct, @verify_correct, x25519_correct'). -Print Assumptions three_correct.
\ No newline at end of file +Print Assumptions three_correct. |