diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-12-24 09:41:21 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2018-01-09 10:09:46 -0500 |
| commit | fd6a2cd64f16da8dfb7d5dec8d892ade0c21c6cb (patch) | |
| tree | dcceb0302bbbe56568c97b23cdd52c0c326e9cfa /src/Curves | |
| parent | c46e776eca741f462c13a130a28eedabbef5001e (diff) | |
Jabobian.v: par -> all
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Weierstrass/Jacobian.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Curves/Weierstrass/Jacobian.v b/src/Curves/Weierstrass/Jacobian.v index a2d5df013..323816b81 100644 --- a/src/Curves/Weierstrass/Jacobian.v +++ b/src/Curves/Weierstrass/Jacobian.v @@ -212,7 +212,7 @@ Module Jacobian. {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12} (* TODO: why do we need 12 instead of 3? *) P Q : W.eq (to_affine (add P Q)) (W.add (to_affine P) (to_affine Q)). - Proof. prept; trivial; try contradiction. Time par: abstract t. Time Qed. + Proof. prept; trivial; try contradiction. Time all: abstract t. Time Qed. (* 306.478 secs (43.916u,1.032s) ;; 18.857 secs (18.856u,0.008s) *) End AEqMinus3. End Jacobian. |