diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec
index df0e3127f..2d7e57ff8 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 (/).