From fb7760da85a6957b6c1fc757f107be907161434d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 18 Feb 2026 10:50:10 +0100 Subject: [PATCH] Adapt to Rocq PR # 20985 (backward compatible hint) --- theories/micromega/Tauto.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index 27b2621475..3790039c1c 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -289,7 +289,8 @@ Section S. End S. - +#[global] +Hint Extern 2 (subrelation (eiff _) _) => progress cbn : typeclass_instances. (** Typical boolean formulae *) Definition eKind (k: kind) := if k then Prop else bool.