From 2727f675a252b38cd432c8ade216fe259faae2df Mon Sep 17 00:00:00 2001
From: Benjamin Gregoire <Benjamin.Gregoire@inria.fr>
Date: Tue, 10 Nov 2026 19:54:59 +0100
Subject: [PATCH] algebra(ZModP): clone ZModpField with <= substitutions

The type and operators of the field structure are now substituted with
<= instead of <-, so that ZModpField keeps them and can be passed as a
theory, e.g. theory IDCoeff <- ZModpField when cloning Poly.Poly.
---
 theories/algebra/ZModP.ec | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec
index df0e3127f9..2d7e57ff8e 100644
--- a/theories/algebra/ZModP.ec
+++ b/theories/algebra/ZModP.ec
@@ -303,14 +303,14 @@ by move: nz_x; rewrite -asint_eq zeroE pmod_small // rg_asint.
 qed.
 
 clone import Ring.Field as ZModpField with
-  type t     <- zmod,
-  op   zeror <- zero,
-  op   oner  <- one,
-  op   ( + ) <- ( + ),
-  op   [ - ] <- ([-]),
-  op   ( * ) <- ( * ),
-  op   invr  <- inv,
-  op   exp   <- ZModpRing.exp
+  type t     <= zmod,
+  op   zeror <= zero,
+  op   oner  <= one,
+  op   ( + ) <= ( + ),
+  op   [ - ] <= ([-]),
+  op   ( * ) <= ( * ),
+  op   invr  <= inv,
+  op   exp   <= ZModpRing.exp
   proof *
   remove abbrev (-)
   remove abbrev (/).