try fix CI error on coq8.20

math-comp · Aug 13, 2024 · 4fd9bd8 · 4fd9bd8
1 parent 1e43187
commit 4fd9bd8
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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}) :