Compatible with MathComp dev (2.1)

coq-community · Oct 14, 2023 · 5d201fa · 5d201fa
1 parent 6d7edfb
commit 5d201fa
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/hanson.v b/theories/hanson.v
@@ -540,7 +540,7 @@ suff [K [Kpos KP]] : exists K : rat,
   suff: (C n m.+1)%:R <= (k%:Q + 1) * 3%:R ^ n.
     by rewrite -[_ + 1%:R]natrD -[_ ^ n]natrX -natrM ler_nat addn1.
   exact/le_trans/ler_wpM2r/ltW/leKSn/exprz_ge0.
-move mE: 10%:Q => m.
+move mE: 10%N%:Q => m. (* FIXME *)
 have lt0m : 0 < m by rewrite -mE.
 have le0m : 0 <= m by exact: ltW.
 have lt1m : 1 < m by rewrite -mE.