diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-21 18:01:18 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | f5c6a57c1453249aac448a33ac3443e45a0d3222 (patch) | |
| tree | 72919ee54472c746feab4b51898095ae5caad768 /src/Spec | |
| parent | c1c764ead6291e25f6da3508f1ae2b46c1e574d4 (diff) | |
rewrite ExtendedCoordinates, fix Ed25519
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/Ed25519.v | 11 |
1 files changed, 9 insertions, 2 deletions
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. |