From 969b32d07e9bae4e0d932b968efdc03d4a637e91 Mon Sep 17 00:00:00 2001
From: thery <Laurent.Thery@inria.fr>
Date: Thu, 2 Nov 2023 13:59:43 +0100
Subject: [PATCH] functor behavior

---
 elliptic.v | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/elliptic.v b/elliptic.v
index 1c891d3..6ea1062 100644
--- 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.