Adapt to coq/coq#18880

coq-community · Apr 11, 2024 · 7b7e3a0 · 7b7e3a0
1 parent 17b7a31
commit 7b7e3a0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)}.