diff options
| author |  Andres Erbsen <andreser@google.com> | 2017-12-14 10:57:35 -0500 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2018-01-09 10:09:46 -0500 |
| commit | c46e776eca741f462c13a130a28eedabbef5001e (patch) | |
| tree | 2c8cc724bc5740073e9ce31d3f81f05190aa9531 /src/Curves | |
| parent | 32133752a3d4ab3bae14df49921c9ad1e73fae5e (diff) | |
src/Curves/Weierstrass/Jacobian.v: specialized destruct_head_*
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Weierstrass/Jacobian.v | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/src/Curves/Weierstrass/Jacobian.v b/src/Curves/Weierstrass/Jacobian.v index d264b243b..a2d5df013 100644 --- a/src/Curves/Weierstrass/Jacobian.v +++ b/src/Curves/Weierstrass/Jacobian.v @@ -39,13 +39,14 @@ Module Jacobian. | _ => progress specialize_by trivial | _ => progress cbv [proj1_sig fst snd] | _ => progress autounfold with points_as_coordinates in * - | _ => progress destruct_head' @unit - | _ => progress destruct_head' @bool - | _ => progress destruct_head' @prod - | _ => progress destruct_head' @sig - | _ => progress destruct_head' @sum - | _ => progress destruct_head' @and - | _ => progress destruct_head' @or + | _ => progress destruct_head'_True + | _ => progress destruct_head'_unit + | _ => progress destruct_head'_prod + | _ => progress destruct_head'_sig + | _ => progress destruct_head'_and + | _ => progress destruct_head'_sum + | _ => progress destruct_head'_bool + | _ => progress destruct_head'_or | H: context[dec ?P] |- _ => destruct (dec P) | |- context[dec ?P] => destruct (dec P) | |- ?P => lazymatch type of P with Prop => split end @@ -212,7 +213,7 @@ Module Jacobian. 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. - (* 514.584 secs (69.907u,1.052s) ;; 30.65 secs (30.516u,0.024s*) + (* 306.478 secs (43.916u,1.032s) ;; 18.857 secs (18.856u,0.008s) *) End AEqMinus3. End Jacobian. End Jacobian. |