From 4fd9bd8ebd6da076ebf4448d3225d1e6615f6ee6 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Tue, 13 Aug 2024 13:16:03 +0200
Subject: [PATCH] try fix CI error on coq8.20

---
 cylinder.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/cylinder.v b/cylinder.v
index 1ab498c..4618850 100644
--- a/cylinder.v
+++ b/cylinder.v
@@ -1397,7 +1397,7 @@ Qed.
 Definition elimp_subdef1 n (P : {fset {mpoly R[n.+1]}}) :=
   \big[fsetU/fset0]_(p : P) truncations (muni (val p)).
 
-Definition elimp_subdef2 n (P : {fset {mpoly R[n.+1]}}) :=
+Definition elimp_subdef2 n (P : {fset {mpoly R[n.+1]}}) : {fset {mpoly R[n]}} :=
   \big[fsetU/fset0]_(p : elimp_subdef1 P | (3 <= size (val p))%N)
       [fset subresultant (val j) (val p) (val p)^`() |
           j : 'I_(size (val p)).-2].
@@ -1420,7 +1420,7 @@ Definition elimp_subdef5 n (P : {fset {mpoly R[n.+1]}}) :=
 
 Definition elimp n (P : {fset {mpoly R[n.+1]}}) :=
   [fset p in elimp_subdef2 P `|` elimp_subdef3 P
-      (* `|` elimp_subdef4 P *) `|` elimp_subdef5 P | (1 < msize (val p))%N].
+      (* `|` elimp_subdef4 P *) `|` elimp_subdef5 P | (1 < msize p)%N].
 
 Lemma map_poly_truncate (A B : ringType) (f : {rmorphism A -> B}) d
     (p : {poly A}) :