From cda9c2b4c4c214d81440b6e957fb10c483e80b1c Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Wed, 31 Jan 2024 09:50:18 +0100
Subject: [PATCH] Fix removing of null_fun_head

---
 3rdparty/ALEA/Qmeasure.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/3rdparty/ALEA/Qmeasure.v b/3rdparty/ALEA/Qmeasure.v
index 52f619d..8e242d6 100644
--- 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.