From 497ac4e2e7e331c48eddfd428f2287c5384c9c08 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 10 Nov 2016 14:09:59 -0500 Subject: Work around looping in 8.4 This fixes #96 --- src/Experiments/Ed25519.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/Experiments') 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. -- cgit v1.2.3