diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-03-03 16:09:34 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-03-03 16:09:34 -0500 |
| commit | 2fa2df7f86b39edfb6d817954c1a5332c4e1a431 (patch) | |
| tree | 92f22995e846fc6c14eefbfa0d7bb6cd64b25264 /src/ModularArithmetic/PrimeFieldTheorems.v | |
| parent | fc7a0870a4e93e9410f4b1da94357c4802110212 (diff) | |
CompleteEdwardsCurveTheorems: associativity proof that times out on Qed
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index e32b4b093..40af15dac 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -324,8 +324,8 @@ Section VariousModPrime. apply F_add_reg_l in opp_spec; auto. Qed. - Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq. - Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops. + Global Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq. + Global Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops. Proof. econstructor; eauto with typeclass_instances; unfold R2, equality, eq_notation, addition, add_notation, one, one_notation, @@ -333,12 +333,12 @@ Section VariousModPrime. sub_notation, opposite, opp_notation; intros; ring. Qed. - Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring. + Global Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring. Proof. repeat intro. apply F_mul_comm. Qed. - Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring. + Global Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring. Proof. econstructor; eauto using Fq_mul_zero_why, Fq_1_neq_0. Qed. |