From f5c6a57c1453249aac448a33ac3443e45a0d3222 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 21 Feb 2017 18:01:18 -0500 Subject: rewrite ExtendedCoordinates, fix Ed25519 --- src/Spec/Ed25519.v | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 45179a81e..02f59c9e5 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -83,6 +83,13 @@ Section Ed25519. (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512). Proof. split; try exact _. - timeout 1 match goal with H:?P |- ?P => idtac end. - Admitted. + (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *) + (* timeout 1 match goal with H:?P |- ?P => idtac end. *) + Crypto.Util.Decidable.vm_decide. + Crypto.Util.Decidable.vm_decide. + Crypto.Util.Decidable.vm_decide. + Crypto.Util.Decidable.vm_decide. + Crypto.Util.Decidable.vm_decide. + exact l_order_B. + Qed. End Ed25519. -- cgit v1.2.3