Fix removing of null_fun_head

math-comp · Jan 31, 2024 · cda9c2b · cda9c2b
1 parent 29d011a
commit cda9c2b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/3rdparty/ALEA/Qmeasure.v b/3rdparty/ALEA/Qmeasure.v
@@ -127,10 +127,10 @@ Hint Resolve Mstable0 : core.
 Lemma Mstable_opp : stable_opp m.
 Proof using Mstable_sub.
 move => f; transitivity (m \0 - m f); first last.
-  by rewrite Mstable0 /null_fun_head /= sub0r.
+  by rewrite Mstable0 /= sub0r.
 rewrite -Mstable_sub.
 apply Mstable_eq => x.
-by rewrite /null_fun_head /= sub0r.
+by rewrite /= sub0r.
 Qed.
 
 Lemma Mstable_add : stable_add m.