functor behavior

thery · Nov 2, 2023 · 969b32d · 969b32d
1 parent 2e6ef90
commit 969b32d
Showing 1 changed file with 7 additions and 5 deletions.
diff --git a/elliptic.v b/elliptic.v
@@ -1028,10 +1028,16 @@ move=> [|x y e] //=; case: eqP => // p1.
 by congr (Some _); apply: curve_elt_irr.
 Qed.
 
+HB.instance Definition _ := 
+  Choice.copy elt (pcan_type elt_pcancel).
+
+Definition ell_Zmod := GRing.isZmodule.Build elt addeA  addeC add0e addNe.
+
 End ELLIPTIC.
 
 Section ELLIPTIC_FINE.
 
+
 (******************************************************************************)
 (*                                                                            *)
 (*      K is finite                                                           *)
@@ -1042,11 +1048,7 @@ Variable K : finFieldType.
 Variable A B : K.
 Variable Eth : ell_theory A B.
 
-HB.instance Definition _ := 
-  Choice.copy (elt A B) (pcan_type (@elt_pcancel K A B)).
-HB.instance Definition _ := 
-  GRing.isZmodule.Build (elt A B) 
-   (addeA Eth) (addeC Eth) (add0e Eth) (addNe Eth).
+HB.instance Definition _ := ell_Zmod Eth. 
 
 Open Scope ring_scope.