memo

Author: affeldt-aist

changelog.txt

@@ -1,3 +1,9 @@
+-------------------
+from 0.9.2 to 0.9.3
+-------------------
+
+- add compatibility with MathComp 2.4.0 (with Coq 8.20)
+
 -------------------
 from 0.9.1 to 0.9.2
 -------------------

lib/realType_ext.v

@@ -135,7 +135,7 @@ Proof. by field. Qed.
 Lemma x_x2_max {R : realFieldType} (q : R) : q * (1 - q) <= 4^-1.
 Proof.
 rewrite x_x2_eq.
-have : forall a b : R, 0 <= b -> a - b <= a. move=>  *; lra.
+have : forall a b : R, 0 <= b -> a - b <= a. move=> *; lra.
 apply; apply mulr_ge0; [lra | exact: exprn_even_ge0].
 Qed.