From 7b7e3a0320eef1c024eb9088ffe7f0bd1eb60f5f Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 11 Apr 2024 14:59:22 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18880

---
 varieties/empty.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/varieties/empty.v b/varieties/empty.v
index 4836b48..ef793b5 100644
--- a/varieties/empty.v
+++ b/varieties/empty.v
@@ -11,7 +11,7 @@ Definition Laws (_: EqEntailment sig): Prop := False.
 
 Definition theory: EquationalTheory := Build_EquationalTheory sig Laws.
 
-Let carriers := False_rect _: sorts sig → Type.
+#[local] Definition carriers := False_rect _: sorts sig → Type.
 
 #[global]
 Instance: `{Equiv (carriers a)}.