Merge pull request #237 from mattam82/rewrite-in-lets

Adapt to Rocq PR # 20985 (backward compatible hint)

Author: SkySkimmer

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.