From dbe86b2eed07a16125411d078e0eaf88d7c1818d Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>
Date: Wed, 8 Jul 2026 11:54:04 +0200
Subject: [PATCH] PolyReduceZp: use default clone overrides (`<=`) and drop
 redundant `p` param

---
 theories/algebra/PolyReduce.ec | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/theories/algebra/PolyReduce.ec b/theories/algebra/PolyReduce.ec
index 57fc01497..ea679bf93 100644
--- a/theories/algebra/PolyReduce.ec
+++ b/theories/algebra/PolyReduce.ec
@@ -463,15 +463,11 @@ end PolyReduce.
 abstract theory PolyReduceZp.
 type coeff.
 
-op p : { int | 2 <= p } as ge2_p.
-
-clone import ZModRing as Zp with
-    op    p     <= p
-    proof ge2_p by exact/ge2_p.
+clone import ZModRing as Zp.
 
 clone import PolyReduce with
-    type coeff <- Zp.zmod,
-  theory Coeff <- ZModpRing.
+    type coeff <= Zp.zmod,
+  theory Coeff <= ZModpRing.
 
 (* ==================================================================== *)
 (* We already know that polyXnD1 is finite. However, we prove here that *)