diff options
Diffstat (limited to 'src/Spec/WeierstrassCurve.v')
| -rw-r--r-- | src/Spec/WeierstrassCurve.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 7ec5d99ec..e2c99a8fe 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -11,8 +11,8 @@ Module E. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - Local Infix "=?" := Algebra.eq_dec (at level 70, no associativity) : type_scope. - Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Algebra.eq_dec x y)) : bool_scope. + Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope. + Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "- x" := (Fopp x). |