Workaround universe issue

math-comp · Apr 12, 2023 · 9f0ffef · 9f0ffef
1 parent 2578d01
commit 9f0ffef
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
@@ -108,8 +108,11 @@ apply: eq_bigr => j1 _; rewrite coefM; apply: eq_bigr=> i1 _.
 by rewrite !coef_swapXY.
 Qed.
 HB.instance Definition _ :=
-  GRing.isMultiplicative.Build (poly (poly R)) (poly (poly R)) swapXY
+  GRing.isMultiplicative.Build
+    (poly [the semiRingType of poly R]) (poly [the semiRingType of poly R])
+    swapXY
     swapXY_is_multiplicative.
+(* TODO_HB: fix HB to remove the [semiRIngType of _] above *)
 
 Lemma swapXY_is_scalable : scalable_for (map_poly polyC \; *%R) swapXY.
 Proof. by move=> p u /=; rewrite -mul_polyC rmorphM /= swapXY_polyC. Qed.