diff options
Diffstat (limited to 'src/Curves/Edwards')
| -rw-r--r-- | src/Curves/Edwards/AffineProofs.v | 7 | ||||
| -rw-r--r-- | src/Curves/Edwards/XYZT.v | 7 |
2 files changed, 11 insertions, 3 deletions
diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v index e77e39f50..8e69b78fe 100644 --- a/src/Curves/Edwards/AffineProofs.v +++ b/src/Curves/Edwards/AffineProofs.v @@ -44,7 +44,7 @@ Module E. Local Notation mul := (E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)). - Next Obligation. destruct P as [ [??]?]; cbv; fsatz. Qed. + Next Obligation. match goal with P : point |- _ => destruct P as [ [??]?] end; cbv; fsatz. Qed. Ltac t_step := match goal with @@ -203,7 +203,10 @@ Module E. cbv [compress decompress exist_option coordinates] in *; intros. t. intro. - apply (H0 f); [|congruence]. + match goal with + | [ H0 : _ |- False ] + => apply (H0 f); [|congruence] + end. admit. intro. Prod.inversion_prod; subst. rewrite solve_correct in y. diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v index 2b126dfcb..3604e9b2e 100644 --- a/src/Curves/Edwards/XYZT.v +++ b/src/Curves/Edwards/XYZT.v @@ -105,7 +105,12 @@ Module Extended. let Z3 := F*G in (X3, Y3, Z3, T3) end. - Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2))); t. Qed. + Next Obligation. + match goal with + | [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ] + => pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2))) + end; t. + Qed. Global Instance isomorphic_commutative_group_m1 : @Group.isomorphic_commutative_groups |