diff options
author | jadep <jade.philipoom@gmail.com> | 2016-08-24 15:49:01 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-08-24 15:49:01 -0400 |
commit | 25b95dd8547ec4cef48d55d84f39ee56230d5a1b (patch) | |
tree | 1a890287e94f18778d8d6553db649960efb1beb8 /src/Algebra.v | |
parent | ecd6954da5768ca3d38c7c52c6ac40b2b24d41a6 (diff) | |
parent | 579a64242f2ccf37db6c16b0aa674c78c3433c00 (diff) |
Merge branch 'fast-inverse'
Diffstat (limited to 'src/Algebra.v')
-rw-r--r-- | src/Algebra.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 04598989a..fd903825e 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -364,14 +364,12 @@ Module ScalarMult. Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. Proof. - repeat intro; subst; - match goal with [n:nat |- _ ] => - solve [induction n; simpl scalarmult_ref; rewrite_hyp ?*; reflexivity] - end. + repeat intro; subst. + match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end. + repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity. Qed. Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. - Proof. induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). Qed. |