From 458b04c190057552f027cf91c0d52835cebdb569 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 15 Oct 2026 14:56:39 +0200 Subject: [PATCH] Fix scope warning in MSetRBT ifpred abbreviation --- theories/MSets/MSetRBT.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index 1b7fbda601..b1aecf6eef 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -964,7 +964,7 @@ Qed. (** ** Treeify *) -Abbreviation ifpred p n := (if p then pred n else n%nat). +Abbreviation ifpred p n := (if p then pred n else n%_nat). Definition treeify_invariant size (f:treeify_t) := forall acc,